Theorem mpet2 37058

Description: Member Partition-Equivalence Theorem in a shorter form. Together with mpet 37057 mpet3 37054, mostly in its conventional cpet 37056 and cpet2 37055 form, 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
mpet2	⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)

Proof of Theorem mpet2

Step	Hyp	Ref	Expression
1		mpet 37057	. 2 ⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
2		df-membpart 36986	. 2 ⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
3		df-comember 36884	. 2 ⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
4	1, 2, 3	3bitr3i 300	1 ⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)

Syntax hints:   ↔ wb 205   E cep 5512  ^◡ccnv 5606   ↾ cres 5609   ≀ ccoss 36389   ErALTV werALTV 36415   CoMembEr wcomember 36417   Part wpart 36428   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:  mpets2  37059