Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cpet Structured version   Visualization version   GIF version

Theorem cpet 38817
Description: The conventional form of Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have been calling disjoint or partition what we call element disjoint or member partition, see also cpet2 38816. Cf. mpet 38818, mpet2 38819 and mpet3 38815 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38830 and pet2 38829 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
Assertion
Ref Expression
cpet ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))

Proof of Theorem cpet
StepHypRef Expression
1 dfmembpart2 38749 . 2 ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
2 cpet2 38816 . 2 (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))
31, 2bitri 275 1 ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395   = wceq 1540  wcel 2108  c0 4332   cuni 4905   / cqs 8740  ccoels 38161   EqvRel weqvrel 38177   ElDisj weldisj 38196   MembPart wmembpart 38201
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-id 5576  df-eprel 5582  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-ec 8743  df-qs 8747  df-coss 38390  df-coels 38391  df-refrel 38491  df-cnvrefrel 38506  df-symrel 38523  df-trrel 38553  df-eqvrel 38564  df-dmqs 38618  df-funALTV 38661  df-disjALTV 38684  df-eldisj 38686  df-part 38745  df-membpart 38747
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator