Step |
Hyp |
Ref |
Expression |
1 |
|
dfsbcq2 |
|- ( z = A -> ( [ z / x ] B e. C <-> [. A / x ]. B e. C ) ) |
2 |
|
dfsbcq2 |
|- ( z = A -> ( [ z / x ] y e. B <-> [. A / x ]. y e. B ) ) |
3 |
2
|
abbidv |
|- ( z = A -> { y | [ z / x ] y e. B } = { y | [. A / x ]. y e. B } ) |
4 |
|
dfsbcq2 |
|- ( z = A -> ( [ z / x ] y e. C <-> [. A / x ]. y e. C ) ) |
5 |
4
|
abbidv |
|- ( z = A -> { y | [ z / x ] y e. C } = { y | [. A / x ]. y e. C } ) |
6 |
3 5
|
eleq12d |
|- ( z = A -> ( { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } ) ) |
7 |
|
nfs1v |
|- F/ x [ z / x ] y e. B |
8 |
7
|
nfab |
|- F/_ x { y | [ z / x ] y e. B } |
9 |
|
nfs1v |
|- F/ x [ z / x ] y e. C |
10 |
9
|
nfab |
|- F/_ x { y | [ z / x ] y e. C } |
11 |
8 10
|
nfel |
|- F/ x { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } |
12 |
|
sbab |
|- ( x = z -> B = { y | [ z / x ] y e. B } ) |
13 |
|
sbab |
|- ( x = z -> C = { y | [ z / x ] y e. C } ) |
14 |
12 13
|
eleq12d |
|- ( x = z -> ( B e. C <-> { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } ) ) |
15 |
11 14
|
sbiev |
|- ( [ z / x ] B e. C <-> { y | [ z / x ] y e. B } e. { y | [ z / x ] y e. C } ) |
16 |
1 6 15
|
vtoclbg |
|- ( A e. _V -> ( [. A / x ]. B e. C <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } ) ) |
17 |
|
df-csb |
|- [_ A / x ]_ B = { y | [. A / x ]. y e. B } |
18 |
|
df-csb |
|- [_ A / x ]_ C = { y | [. A / x ]. y e. C } |
19 |
17 18
|
eleq12i |
|- ( [_ A / x ]_ B e. [_ A / x ]_ C <-> { y | [. A / x ]. y e. B } e. { y | [. A / x ]. y e. C } ) |
20 |
16 19
|
bitr4di |
|- ( A e. _V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) ) |
21 |
|
sbcex |
|- ( [. A / x ]. B e. C -> A e. _V ) |
22 |
21
|
con3i |
|- ( -. A e. _V -> -. [. A / x ]. B e. C ) |
23 |
|
noel |
|- -. [_ A / x ]_ B e. (/) |
24 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ C = (/) ) |
25 |
24
|
eleq2d |
|- ( -. A e. _V -> ( [_ A / x ]_ B e. [_ A / x ]_ C <-> [_ A / x ]_ B e. (/) ) ) |
26 |
23 25
|
mtbiri |
|- ( -. A e. _V -> -. [_ A / x ]_ B e. [_ A / x ]_ C ) |
27 |
22 26
|
2falsed |
|- ( -. A e. _V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) ) |
28 |
20 27
|
pm2.61i |
|- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C ) |