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 ) |