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

Metamath Proof Explorer

Theorem csbif

Description: Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013) (Revised by NM, 19-Aug-2018)

Ref Expression
Assertion csbif 
|- [_ A / x ]_ if ( ph , B , C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ if ( ph , B , C ) = [_ A / x ]_ if ( ph , B , C ) )
2 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
4 csbeq1 
 |-  ( y = A -> [_ y / x ]_ C = [_ A / x ]_ C )
5 2 3 4 ifbieq12d 
 |-  ( y = A -> if ( [ y / x ] ph , [_ y / x ]_ B , [_ y / x ]_ C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) )
6 1 5 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ if ( ph , B , C ) = if ( [ y / x ] ph , [_ y / x ]_ B , [_ y / x ]_ C ) <-> [_ A / x ]_ if ( ph , B , C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) ) )
7 vex 
 |-  y e. _V
8 nfs1v 
 |-  F/ x [ y / x ] ph
9 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
10 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
11 8 9 10 nfif 
 |-  F/_ x if ( [ y / x ] ph , [_ y / x ]_ B , [_ y / x ]_ C )
12 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
13 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
14 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
15 12 13 14 ifbieq12d 
 |-  ( x = y -> if ( ph , B , C ) = if ( [ y / x ] ph , [_ y / x ]_ B , [_ y / x ]_ C ) )
16 7 11 15 csbief 
 |-  [_ y / x ]_ if ( ph , B , C ) = if ( [ y / x ] ph , [_ y / x ]_ B , [_ y / x ]_ C )
17 6 16 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ if ( ph , B , C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ if ( ph , B , C ) = (/) )
19 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
20 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
21 19 20 ifeq12d 
 |-  ( -. A e. _V -> if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) = if ( [. A / x ]. ph , (/) , (/) ) )
22 ifid 
 |-  if ( [. A / x ]. ph , (/) , (/) ) = (/)
23 21 22 eqtr2di 
 |-  ( -. A e. _V -> (/) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) )
24 18 23 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ if ( ph , B , C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C ) )
25 17 24 pm2.61i 
 |-  [_ A / x ]_ if ( ph , B , C ) = if ( [. A / x ]. ph , [_ A / x ]_ B , [_ A / x ]_ C )