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

Metamath Proof Explorer

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