Step |
Hyp |
Ref |
Expression |
1 |
|
csbab |
|- [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } |
2 |
|
sbcex2 |
|- ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) |
3 |
|
sbcan |
|- ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) |
4 |
|
sbcg |
|- ( A e. _V -> ( [. A / x ]. z e. y <-> z e. y ) ) |
5 |
4
|
anbi1d |
|- ( A e. _V -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ [. A / x ]. y e. B ) ) ) |
6 |
|
sbcel2 |
|- ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) |
7 |
6
|
anbi2i |
|- ( ( z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) |
8 |
5 7
|
bitrdi |
|- ( A e. _V -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
9 |
3 8
|
syl5bb |
|- ( A e. _V -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
10 |
9
|
exbidv |
|- ( A e. _V -> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
11 |
2 10
|
syl5bb |
|- ( A e. _V -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
12 |
11
|
abbidv |
|- ( A e. _V -> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) |
13 |
1 12
|
eqtrid |
|- ( A e. _V -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) |
14 |
|
df-uni |
|- U. B = { z | E. y ( z e. y /\ y e. B ) } |
15 |
14
|
csbeq2i |
|- [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } |
16 |
|
df-uni |
|- U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } |
17 |
13 15 16
|
3eqtr4g |
|- ( A e. _V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B ) |
18 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ U. B = (/) ) |
19 |
|
csbprc |
|- ( -. A e. _V -> [_ A / x ]_ B = (/) ) |
20 |
19
|
unieqd |
|- ( -. A e. _V -> U. [_ A / x ]_ B = U. (/) ) |
21 |
|
uni0 |
|- U. (/) = (/) |
22 |
20 21
|
eqtr2di |
|- ( -. A e. _V -> (/) = U. [_ A / x ]_ B ) |
23 |
18 22
|
eqtrd |
|- ( -. A e. _V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B ) |
24 |
17 23
|
pm2.61i |
|- [_ A / x ]_ U. B = U. [_ A / x ]_ B |