Step |
Hyp |
Ref |
Expression |
1 |
|
csbeq1 |
|- ( z = A -> [_ z / x ]_ ( iota_ y e. B ph ) = [_ A / x ]_ ( iota_ y e. B ph ) ) |
2 |
|
dfsbcq2 |
|- ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) ) |
3 |
2
|
riotabidv |
|- ( z = A -> ( iota_ y e. B [ z / x ] ph ) = ( iota_ y e. B [. A / x ]. ph ) ) |
4 |
1 3
|
eqeq12d |
|- ( z = A -> ( [_ z / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph ) <-> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) ) ) |
5 |
|
vex |
|- z e. _V |
6 |
|
nfs1v |
|- F/ x [ z / x ] ph |
7 |
|
nfcv |
|- F/_ x B |
8 |
6 7
|
nfriota |
|- F/_ x ( iota_ y e. B [ z / x ] ph ) |
9 |
|
sbequ12 |
|- ( x = z -> ( ph <-> [ z / x ] ph ) ) |
10 |
9
|
riotabidv |
|- ( x = z -> ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph ) ) |
11 |
5 8 10
|
csbief |
|- [_ z / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [ z / x ] ph ) |
12 |
4 11
|
vtoclg |
|- ( A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) ) |
13 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = (/) ) |
14 |
|
df-riota |
|- ( iota_ y e. B [. A / x ]. ph ) = ( iota y ( y e. B /\ [. A / x ]. ph ) ) |
15 |
|
euex |
|- ( E! y ( y e. B /\ [. A / x ]. ph ) -> E. y ( y e. B /\ [. A / x ]. ph ) ) |
16 |
|
sbcex |
|- ( [. A / x ]. ph -> A e. _V ) |
17 |
16
|
adantl |
|- ( ( y e. B /\ [. A / x ]. ph ) -> A e. _V ) |
18 |
17
|
exlimiv |
|- ( E. y ( y e. B /\ [. A / x ]. ph ) -> A e. _V ) |
19 |
15 18
|
syl |
|- ( E! y ( y e. B /\ [. A / x ]. ph ) -> A e. _V ) |
20 |
|
iotanul |
|- ( -. E! y ( y e. B /\ [. A / x ]. ph ) -> ( iota y ( y e. B /\ [. A / x ]. ph ) ) = (/) ) |
21 |
19 20
|
nsyl5 |
|- ( -. A e. _V -> ( iota y ( y e. B /\ [. A / x ]. ph ) ) = (/) ) |
22 |
14 21
|
eqtr2id |
|- ( -. A e. _V -> (/) = ( iota_ y e. B [. A / x ]. ph ) ) |
23 |
13 22
|
eqtrd |
|- ( -. A e. _V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) ) |
24 |
12 23
|
pm2.61i |
|- [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) |