Theorem mpet 37057

Description: Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 37060. Member partition and comember equivalence relation are the same (or: each element of 𝐴 have equivalent comembers if and only if 𝐴 is a member partition). Together with mpet2 37058, mpet3 37054, and with the conventional cpet 37056 and cpet2 37055, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37068 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)

Assertion

Ref	Expression
mpet	⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)

Proof of Theorem mpet

Step	Hyp	Ref	Expression
1		mpet3 37054	. 2 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
2		dfmembpart2 36988	. 2 ⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
3		dfcomember3 36892	. 2 ⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
4	1, 2, 3	3bitr4i 302	1 ⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∅c0 4267  ∪ cuni 4850   / cqs 8545   ∼ ccoels 36390   CoElEqvRel wcoeleqvrel 36408   CoMembEr wcomember 36417   ElDisj weldisj 36425   MembPart wmembpart 36430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3350  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-id 5507  df-eprel 5513  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ec 8548  df-qs 8552  df-coss 36629  df-coels 36630  df-refrel 36730  df-cnvrefrel 36745  df-symrel 36762  df-trrel 36792  df-eqvrel 36803  df-coeleqvrel 36805  df-dmqs 36857  df-erALTV 36882  df-comember 36884  df-funALTV 36900  df-disjALTV 36923  df-eldisj 36925  df-part 36984  df-membpart 36986

This theorem is referenced by:  mpet2  37058  mainpart  37061  fences  37062