Theorem bj-mpomptALT

Description: Alternate proof of mpompt . (Contributed by BJ, 30-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bj-mpomptALT.1	|- ( z = <. x , y >. -> C = D )
Assertion	bj-mpomptALT	|- ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> D )

Proof

Step	Hyp	Ref	Expression
1		bj-mpomptALT.1	|- ( z = <. x , y >. -> C = D )
2		elxp2	|- ( z e. ( A X. B ) <-> E. x e. A E. y e. B z = <. x , y >. )
3	2	anbi1i	|- ( ( z e. ( A X. B ) /\ t = C ) <-> ( E. x e. A E. y e. B z = <. x , y >. /\ t = C ) )
4		r19.41v	|- ( E. x e. A ( E. y e. B z = <. x , y >. /\ t = C ) <-> ( E. x e. A E. y e. B z = <. x , y >. /\ t = C ) )
5		r19.41v	|- ( E. y e. B ( z = <. x , y >. /\ t = C ) <-> ( E. y e. B z = <. x , y >. /\ t = C ) )
6	1	eqeq2d	|- ( z = <. x , y >. -> ( t = C <-> t = D ) )
7	6	pm5.32i	|- ( ( z = <. x , y >. /\ t = C ) <-> ( z = <. x , y >. /\ t = D ) )
8	7	rexbii	|- ( E. y e. B ( z = <. x , y >. /\ t = C ) <-> E. y e. B ( z = <. x , y >. /\ t = D ) )
9	5 8	bitr3i	|- ( ( E. y e. B z = <. x , y >. /\ t = C ) <-> E. y e. B ( z = <. x , y >. /\ t = D ) )
10	9	rexbii	|- ( E. x e. A ( E. y e. B z = <. x , y >. /\ t = C ) <-> E. x e. A E. y e. B ( z = <. x , y >. /\ t = D ) )
11	3 4 10	3bitr2i	|- ( ( z e. ( A X. B ) /\ t = C ) <-> E. x e. A E. y e. B ( z = <. x , y >. /\ t = D ) )
12	11	opabbii	|- { <. z , t >. | ( z e. ( A X. B ) /\ t = C ) } = { <. z , t >. | E. x e. A E. y e. B ( z = <. x , y >. /\ t = D ) }
13		df-mpt	|- ( z e. ( A X. B ) |-> C ) = { <. z , t >. | ( z e. ( A X. B ) /\ t = C ) }
14		bj-dfmpoa	|- ( x e. A , y e. B |-> D ) = { <. z , t >. | E. x e. A E. y e. B ( z = <. x , y >. /\ t = D ) }
15	12 13 14	3eqtr4i	|- ( z e. ( A X. B ) |-> C ) = ( x e. A , y e. B |-> D )