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

Metamath Proof Explorer

Theorem fvopab6

Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses fvopab6.1 
|- F = { <. x , y >. | ( ph /\ y = B ) }
fvopab6.2 
|- ( x = A -> ( ph <-> ps ) )
fvopab6.3 
|- ( x = A -> B = C )
Assertion fvopab6 
|- ( ( A e. D /\ C e. R /\ ps ) -> ( F ` A ) = C )

Proof

Step Hyp Ref Expression
1 fvopab6.1 
 |-  F = { <. x , y >. | ( ph /\ y = B ) }
2 fvopab6.2 
 |-  ( x = A -> ( ph <-> ps ) )
3 fvopab6.3 
 |-  ( x = A -> B = C )
4 elex 
 |-  ( A e. D -> A e. _V )
5 3 eqeq2d 
 |-  ( x = A -> ( y = B <-> y = C ) )
6 2 5 anbi12d 
 |-  ( x = A -> ( ( ph /\ y = B ) <-> ( ps /\ y = C ) ) )
7 iba 
 |-  ( y = C -> ( ps <-> ( ps /\ y = C ) ) )
8 7 bicomd 
 |-  ( y = C -> ( ( ps /\ y = C ) <-> ps ) )
9 moeq 
 |-  E* y y = B
10 9 moani 
 |-  E* y ( ph /\ y = B )
11 10 a1i 
 |-  ( x e. _V -> E* y ( ph /\ y = B ) )
12 vex 
 |-  x e. _V
13 12 biantrur 
 |-  ( ( ph /\ y = B ) <-> ( x e. _V /\ ( ph /\ y = B ) ) )
14 13 opabbii 
 |-  { <. x , y >. | ( ph /\ y = B ) } = { <. x , y >. | ( x e. _V /\ ( ph /\ y = B ) ) }
15 1 14 eqtri 
 |-  F = { <. x , y >. | ( x e. _V /\ ( ph /\ y = B ) ) }
16 6 8 11 15 fvopab3ig 
 |-  ( ( A e. _V /\ C e. R ) -> ( ps -> ( F ` A ) = C ) )
17 4 16 sylan 
 |-  ( ( A e. D /\ C e. R ) -> ( ps -> ( F ` A ) = C ) )
18 17 3impia 
 |-  ( ( A e. D /\ C e. R /\ ps ) -> ( F ` A ) = C )