Theorem mpet 37053

Description: Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 37056. 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 37054, mpet3 37050, and with the conventional cpet 37052 and cpet2 37051, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37064 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 37050	. 2 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
2		dfmembpart2 36984	. 2 ⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
3		dfcomember3 36888	. 2 ⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
4	1, 2, 3	3bitr4i 303	1 ⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  ∅c0 4262  ∪ cuni 4844   / cqs 8528   ∼ ccoels 36382   CoElEqvRel wcoeleqvrel 36400   CoMembEr wcomember 36409   ElDisj weldisj 36417   MembPart wmembpart 36422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3331  df-rab 3333  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-id 5500  df-eprel 5506  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-ec 8531  df-qs 8535  df-coss 36625  df-coels 36626  df-refrel 36726  df-cnvrefrel 36741  df-symrel 36758  df-trrel 36788  df-eqvrel 36799  df-coeleqvrel 36801  df-dmqs 36853  df-erALTV 36878  df-comember 36880  df-funALTV 36896  df-disjALTV 36919  df-eldisj 36921  df-part 36980  df-membpart 36982

This theorem is referenced by:  mpet2  37054  mainpart  37057  fences  37058