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 )