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

Metamath Proof Explorer

Theorem cdleme31se

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 26-Feb-2013)

Ref Expression
Hypotheses cdleme31se.e 
|- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ T ) ./\ W ) ) )
cdleme31se.y 
|- Y = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ T ) ./\ W ) ) )
Assertion cdleme31se 
|- ( R e. A -> [_ R / s ]_ E = Y )

Proof

Step Hyp Ref Expression
1 cdleme31se.e 
 |-  E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ T ) ./\ W ) ) )
2 cdleme31se.y 
 |-  Y = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ T ) ./\ W ) ) )
3 nfcvd 
 |-  ( R e. A -> F/_ s ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ T ) ./\ W ) ) ) )
4 oveq1 
 |-  ( s = R -> ( s .\/ T ) = ( R .\/ T ) )
5 4 oveq1d 
 |-  ( s = R -> ( ( s .\/ T ) ./\ W ) = ( ( R .\/ T ) ./\ W ) )
6 5 oveq2d 
 |-  ( s = R -> ( D .\/ ( ( s .\/ T ) ./\ W ) ) = ( D .\/ ( ( R .\/ T ) ./\ W ) ) )
7 6 oveq2d 
 |-  ( s = R -> ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ T ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ T ) ./\ W ) ) ) )
8 3 7 csbiegf 
 |-  ( R e. A -> [_ R / s ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ T ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ T ) ./\ W ) ) ) )
9 1 csbeq2i 
 |-  [_ R / s ]_ E = [_ R / s ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ T ) ./\ W ) ) )
10 8 9 2 3eqtr4g 
 |-  ( R e. A -> [_ R / s ]_ E = Y )