Theorem mpet2 39275

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

Syntax hints:   ↔ wb 206   E cep 5530  ^◡ccnv 5630   ↾ cres 5633   ≀ ccoss 38504   ErALTV werALTV 38530   CoMembEr wcomember 38534   Part wpart 38545   MembPart wmembpart 38547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-eprel 5531  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ec 8645  df-qs 8649  df-coss 38822  df-coels 38823  df-refrel 38913  df-cnvrefrel 38928  df-symrel 38945  df-trrel 38979  df-eqvrel 38990  df-coeleqvrel 38992  df-dmqs 39044  df-erALTV 39070  df-comember 39072  df-funALTV 39088  df-disjALTV 39111  df-eldisj 39113  df-part 39190  df-membpart 39192

This theorem is referenced by:  mpets2  39276