feat(set_theory/zfc): basic lemmas on `pSet.equiv` (#15211)
feat(set_theory/zfc): basic lemmas on `pSet.equiv` (#15211)

We unfold the complex definition into something easier to use.





leanprover-community/mathlib,leanprover-community/mathlib