| 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 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.) |
| Ref | Expression |
|---|---|
| cpet | ⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfmembpart2 38749 | . 2 ⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | |
| 2 | cpet2 38816 | . 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 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 |