Metamath Proof Explorer

Theorem bj-dfmpoa

Description: An equivalent definition of df-mpo . (Contributed by BJ, 30-Dec-2020)

Ref Expression
Assertion bj-dfmpoa 
|- ( x e. A , y e. B |-> C ) = { <. s , t >. | E. x e. A E. y e. B ( s = <. x , y >. /\ t = C ) }

Proof

Step Hyp Ref Expression
1 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , t >. | ( ( x e. A /\ y e. B ) /\ t = C ) }
2 dfoprab2 
 |-  { <. <. x , y >. , t >. | ( ( x e. A /\ y e. B ) /\ t = C ) } = { <. s , t >. | E. x E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) }
3 ancom 
 |-  ( ( ( x e. A /\ y e. B ) /\ t = C ) <-> ( t = C /\ ( x e. A /\ y e. B ) ) )
4 3 anbi2i 
 |-  ( ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> ( s = <. x , y >. /\ ( t = C /\ ( x e. A /\ y e. B ) ) ) )
5 anass 
 |-  ( ( ( s = <. x , y >. /\ t = C ) /\ ( x e. A /\ y e. B ) ) <-> ( s = <. x , y >. /\ ( t = C /\ ( x e. A /\ y e. B ) ) ) )
6 an13 
 |-  ( ( ( s = <. x , y >. /\ t = C ) /\ ( x e. A /\ y e. B ) ) <-> ( y e. B /\ ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) ) )
7 4 5 6 3bitr2i 
 |-  ( ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> ( y e. B /\ ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) ) )
8 7 exbii 
 |-  ( E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> E. y ( y e. B /\ ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) ) )
9 df-rex 
 |-  ( E. y e. B ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) <-> E. y ( y e. B /\ ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) ) )
10 r19.42v 
 |-  ( E. y e. B ( x e. A /\ ( s = <. x , y >. /\ t = C ) ) <-> ( x e. A /\ E. y e. B ( s = <. x , y >. /\ t = C ) ) )
11 8 9 10 3bitr2i 
 |-  ( E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> ( x e. A /\ E. y e. B ( s = <. x , y >. /\ t = C ) ) )
12 11 exbii 
 |-  ( E. x E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> E. x ( x e. A /\ E. y e. B ( s = <. x , y >. /\ t = C ) ) )
13 df-rex 
 |-  ( E. x e. A E. y e. B ( s = <. x , y >. /\ t = C ) <-> E. x ( x e. A /\ E. y e. B ( s = <. x , y >. /\ t = C ) ) )
14 12 13 bitr4i 
 |-  ( E. x E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) <-> E. x e. A E. y e. B ( s = <. x , y >. /\ t = C ) )
15 14 opabbii 
 |-  { <. s , t >. | E. x E. y ( s = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ t = C ) ) } = { <. s , t >. | E. x e. A E. y e. B ( s = <. x , y >. /\ t = C ) }
16 1 2 15 3eqtri 
 |-  ( x e. A , y e. B |-> C ) = { <. s , t >. | E. x e. A E. y e. B ( s = <. x , y >. /\ t = C ) }