Metamath Proof Explorer

Theorem fnwe2val

Description: Lemma for fnwe2 . Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su 
|- ( z = ( F ` x ) -> S = U )
fnwe2.t 
|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
Assertion fnwe2val 
|- ( a T b <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )

Proof

Step Hyp Ref Expression
1 fnwe2.su 
 |-  ( z = ( F ` x ) -> S = U )
2 fnwe2.t 
 |-  T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
3 vex 
 |-  a e. _V
4 vex 
 |-  b e. _V
5 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
6 fveq2 
 |-  ( y = b -> ( F ` y ) = ( F ` b ) )
7 5 6 breqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( F ` x ) R ( F ` y ) <-> ( F ` a ) R ( F ` b ) ) )
8 5 6 eqeqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( F ` x ) = ( F ` y ) <-> ( F ` a ) = ( F ` b ) ) )
9 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
10 fvex 
 |-  ( F ` x ) e. _V
11 10 1 csbie 
 |-  [_ ( F ` x ) / z ]_ S = U
12 5 csbeq1d 
 |-  ( x = a -> [_ ( F ` x ) / z ]_ S = [_ ( F ` a ) / z ]_ S )
13 11 12 eqtr3id 
 |-  ( x = a -> U = [_ ( F ` a ) / z ]_ S )
14 13 adantr 
 |-  ( ( x = a /\ y = b ) -> U = [_ ( F ` a ) / z ]_ S )
15 simpr 
 |-  ( ( x = a /\ y = b ) -> y = b )
16 9 14 15 breq123d 
 |-  ( ( x = a /\ y = b ) -> ( x U y <-> a [_ ( F ` a ) / z ]_ S b ) )
17 8 16 anbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( F ` x ) = ( F ` y ) /\ x U y ) <-> ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
18 7 17 orbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) ) )
19 3 4 18 2 braba 
 |-  ( a T b <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )