![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > cpet | Structured version Visualization version GIF version |
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 38780. Cf. mpet 38782, mpet2 38783 and mpet3 38779 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38794 and pet2 38793 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.) |
Ref | Expression |
---|---|
cpet | ⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfmembpart2 38713 | . 2 ⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | |
2 | cpet2 38780 | . 2 ⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) | |
3 | 1, 2 | bitri 275 | 1 ⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1535 ∈ wcel 2104 ∅c0 4339 ∪ cuni 4914 / cqs 8737 ∼ ccoels 38123 EqvRel weqvrel 38139 ElDisj weldisj 38158 MembPart wmembpart 38163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5430 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-ral 3058 df-rex 3067 df-rmo 3376 df-rab 3433 df-v 3479 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4915 df-br 5150 df-opab 5212 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 8740 df-qs 8744 df-coss 38354 df-coels 38355 df-refrel 38455 df-cnvrefrel 38470 df-symrel 38487 df-trrel 38517 df-eqvrel 38528 df-dmqs 38582 df-funALTV 38625 df-disjALTV 38648 df-eldisj 38650 df-part 38709 df-membpart 38711 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |