Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. A e. V ->. A e. V ). |
2 |
|
sbcg |
|- ( A e. V -> ( [. A / x ]. z e. y <-> z e. y ) ) |
3 |
1 2
|
e1a |
|- (. A e. V ->. ( [. A / x ]. z e. y <-> z e. y ) ). |
4 |
|
sbcel2 |
|- ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) |
5 |
4
|
a1i |
|- ( A e. V -> ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ) |
6 |
1 5
|
e1a |
|- (. A e. V ->. ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ). |
7 |
|
pm4.38 |
|- ( ( ( [. A / x ]. z e. y <-> z e. y ) /\ ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
8 |
7
|
ex |
|- ( ( [. A / x ]. z e. y <-> z e. y ) -> ( ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) -> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) ) |
9 |
3 6 8
|
e11 |
|- (. A e. V ->. ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
10 |
|
sbcan |
|- ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) |
11 |
10
|
a1i |
|- ( A e. V -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) ) |
12 |
1 11
|
e1a |
|- (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) ). |
13 |
|
bibi1 |
|- ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) -> ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) ) |
14 |
13
|
biimprcd |
|- ( ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) -> ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ) ) |
15 |
9 12 14
|
e11 |
|- (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
16 |
15
|
gen11 |
|- (. A e. V ->. A. y ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
17 |
|
exbi |
|- ( A. y ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) |
18 |
16 17
|
e1a |
|- (. A e. V ->. ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
19 |
|
sbcex2 |
|- ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) |
20 |
19
|
a1i |
|- ( A e. V -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) ) |
21 |
1 20
|
e1a |
|- (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) ). |
22 |
|
bibi1 |
|- ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) -> ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) ) |
23 |
22
|
biimprcd |
|- ( ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) -> ( ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) -> ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ) ) |
24 |
18 21 23
|
e11 |
|- (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
25 |
24
|
gen11 |
|- (. A e. V ->. A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ). |
26 |
|
abbi |
|- ( A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) <-> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) |
27 |
26
|
biimpi |
|- ( A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) -> { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) |
28 |
25 27
|
e1a |
|- (. 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 ) } ). |
29 |
|
csbab |
|- [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } |
30 |
29
|
a1i |
|- ( A e. V -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } ) |
31 |
1 30
|
e1a |
|- (. A e. V ->. [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } ). |
32 |
|
eqeq2 |
|- ( { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) ) |
33 |
32
|
biimpd |
|- ( { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) ) |
34 |
28 31 33
|
e11 |
|- (. 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 ) } ). |
35 |
|
df-uni |
|- U. B = { z | E. y ( z e. y /\ y e. B ) } |
36 |
35
|
ax-gen |
|- A. x U. B = { z | E. y ( z e. y /\ y e. B ) } |
37 |
|
spsbc |
|- ( A e. V -> ( A. x U. B = { z | E. y ( z e. y /\ y e. B ) } -> [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } ) ) |
38 |
1 36 37
|
e10 |
|- (. A e. V ->. [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } ). |
39 |
|
sbceqg |
|- ( A e. V -> ( [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ) ) |
40 |
39
|
biimpd |
|- ( A e. V -> ( [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ) ) |
41 |
1 38 40
|
e11 |
|- (. A e. V ->. [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ). |
42 |
|
eqeq2 |
|- ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } <-> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) ) |
43 |
42
|
biimpd |
|- ( [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } -> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) ) |
44 |
34 41 43
|
e11 |
|- (. A e. V ->. [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ). |
45 |
|
df-uni |
|- U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } |
46 |
|
eqeq2 |
|- ( U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( [_ A / x ]_ U. B = U. [_ A / x ]_ B <-> [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ) ) |
47 |
46
|
biimprcd |
|- ( [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> ( U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } -> [_ A / x ]_ U. B = U. [_ A / x ]_ B ) ) |
48 |
44 45 47
|
e10 |
|- (. A e. V ->. [_ A / x ]_ U. B = U. [_ A / x ]_ B ). |
49 |
48
|
in1 |
|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B ) |