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

Metamath Proof Explorer

Theorem cdleme31sn

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

Ref Expression
Hypotheses cdleme31sn.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme31sn.c 
|- C = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D )
Assertion cdleme31sn 
|- ( R e. A -> [_ R / s ]_ N = C )

Proof

Step Hyp Ref Expression
1 cdleme31sn.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , D )
2 cdleme31sn.c 
 |-  C = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D )
3 nfv 
 |-  F/ s R .<_ ( P .\/ Q )
4 nfcsb1v 
 |-  F/_ s [_ R / s ]_ I
5 nfcsb1v 
 |-  F/_ s [_ R / s ]_ D
6 3 4 5 nfif 
 |-  F/_ s if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D )
7 6 a1i 
 |-  ( R e. A -> F/_ s if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) )
8 breq1 
 |-  ( s = R -> ( s .<_ ( P .\/ Q ) <-> R .<_ ( P .\/ Q ) ) )
9 csbeq1a 
 |-  ( s = R -> I = [_ R / s ]_ I )
10 csbeq1a 
 |-  ( s = R -> D = [_ R / s ]_ D )
11 8 9 10 ifbieq12d 
 |-  ( s = R -> if ( s .<_ ( P .\/ Q ) , I , D ) = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) )
12 7 11 csbiegf 
 |-  ( R e. A -> [_ R / s ]_ if ( s .<_ ( P .\/ Q ) , I , D ) = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) )
13 1 csbeq2i 
 |-  [_ R / s ]_ N = [_ R / s ]_ if ( s .<_ ( P .\/ Q ) , I , D )
14 12 13 2 3eqtr4g 
 |-  ( R e. A -> [_ R / s ]_ N = C )