This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmopab3

Description: The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004)

Ref Expression
Assertion dmopab3 
|- ( A. x e. A E. y ph <-> dom { <. x , y >. | ( x e. A /\ ph ) } = A )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A E. y ph <-> A. x ( x e. A -> E. y ph ) )
2 pm4.71 
 |-  ( ( x e. A -> E. y ph ) <-> ( x e. A <-> ( x e. A /\ E. y ph ) ) )
3 2 albii 
 |-  ( A. x ( x e. A -> E. y ph ) <-> A. x ( x e. A <-> ( x e. A /\ E. y ph ) ) )
4 dmopab 
 |-  dom { <. x , y >. | ( x e. A /\ ph ) } = { x | E. y ( x e. A /\ ph ) }
5 19.42v 
 |-  ( E. y ( x e. A /\ ph ) <-> ( x e. A /\ E. y ph ) )
6 5 abbii 
 |-  { x | E. y ( x e. A /\ ph ) } = { x | ( x e. A /\ E. y ph ) }
7 4 6 eqtri 
 |-  dom { <. x , y >. | ( x e. A /\ ph ) } = { x | ( x e. A /\ E. y ph ) }
8 7 eqeq1i 
 |-  ( dom { <. x , y >. | ( x e. A /\ ph ) } = A <-> { x | ( x e. A /\ E. y ph ) } = A )
9 eqcom 
 |-  ( A = { x | ( x e. A /\ E. y ph ) } <-> { x | ( x e. A /\ E. y ph ) } = A )
10 eqabb 
 |-  ( A = { x | ( x e. A /\ E. y ph ) } <-> A. x ( x e. A <-> ( x e. A /\ E. y ph ) ) )
11 8 9 10 3bitr2ri 
 |-  ( A. x ( x e. A <-> ( x e. A /\ E. y ph ) ) <-> dom { <. x , y >. | ( x e. A /\ ph ) } = A )
12 1 3 11 3bitri 
 |-  ( A. x e. A E. y ph <-> dom { <. x , y >. | ( x e. A /\ ph ) } = A )