Theorem opabex

Description: Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996)

	Ref	Expression
Hypotheses	opabex.1	|- A e. _V
	opabex.2	|- ( x e. A -> E* y ph )
Assertion	opabex	|- { <. x , y >. | ( x e. A /\ ph ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		opabex.1	|- A e. _V
2		opabex.2	|- ( x e. A -> E* y ph )
3		funopab	|- ( Fun { <. x , y >. | ( x e. A /\ ph ) } <-> A. x E* y ( x e. A /\ ph ) )
4		moanimv	|- ( E* y ( x e. A /\ ph ) <-> ( x e. A -> E* y ph ) )
5	2 4	mpbir	|- E* y ( x e. A /\ ph )
6	3 5	mpgbir	|- Fun { <. x , y >. | ( x e. A /\ ph ) }
7		dmopabss	|- dom { <. x , y >. | ( x e. A /\ ph ) } C_ A
8	1 7	ssexi	|- dom { <. x , y >. | ( x e. A /\ ph ) } e. _V
9		funex	|- ( ( Fun { <. x , y >. | ( x e. A /\ ph ) } /\ dom { <. x , y >. | ( x e. A /\ ph ) } e. _V ) -> { <. x , y >. | ( x e. A /\ ph ) } e. _V )
10	6 8 9	mp2an	|- { <. x , y >. | ( x e. A /\ ph ) } e. _V