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		abeq2	|- ( 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 )