Theorem mpet2 39460

Description: Member Partition-Equivalence Theorem in a shorter form. Together with mpet 39459 mpet3 39456, mostly in its conventional cpet 39458 and cpet2 39457 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39470 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 39459	. 2 ⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
2		df-membpart 39377	. 2 ⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)
3		df-comember 39257	. 2 ⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
4	1, 2, 3	3bitr3i 304	1 ⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)

Syntax hints:   ↔ wb 209   E cep 5550  ^◡ccnv 5650   ↾ cres 5653   ≀ ccoss 38689   ErALTV werALTV 38715   CoMembEr wcomember 38719   Part wpart 38730   MembPart wmembpart 38732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-id 5546  df-eprel 5551  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ec 8684  df-qs 8688  df-coss 39007  df-coels 39008  df-refrel 39098  df-cnvrefrel 39113  df-symrel 39130  df-trrel 39164  df-eqvrel 39175  df-coeleqvrel 39177  df-dmqs 39229  df-erALTV 39255  df-comember 39257  df-funALTV 39273  df-disjALTV 39296  df-eldisj 39298  df-part 39375  df-membpart 39377

This theorem is referenced by:  mpets2  39461