Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. A e. V ->. A e. V ). |
2 |
|
sbcel12 |
|- ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) |
3 |
2
|
a1i |
|- ( A e. V -> ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) ) |
4 |
1 3
|
e1a |
|- (. A e. V ->. ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) ). |
5 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ <. w , y >. = <. w , y >. ) |
6 |
1 5
|
e1a |
|- (. A e. V ->. [_ A / x ]_ <. w , y >. = <. w , y >. ). |
7 |
|
eleq1 |
|- ( [_ A / x ]_ <. w , y >. = <. w , y >. -> ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ) |
8 |
6 7
|
e1a |
|- (. A e. V ->. ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ). |
9 |
|
bibi1 |
|- ( ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) -> ( ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) <-> ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ) ) |
10 |
9
|
biimprd |
|- ( ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) -> ( ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) -> ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ) ) |
11 |
4 8 10
|
e11 |
|- (. A e. V ->. ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ). |
12 |
11
|
gen11 |
|- (. A e. V ->. A. w ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ). |
13 |
|
exbi |
|- ( A. w ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) -> ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ) |
14 |
12 13
|
e1a |
|- (. A e. V ->. ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ). |
15 |
|
sbcex2 |
|- ( [. A / x ]. E. w <. w , y >. e. B <-> E. w [. A / x ]. <. w , y >. e. B ) |
16 |
15
|
a1i |
|- ( A e. V -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w [. A / x ]. <. w , y >. e. B ) ) |
17 |
16
|
bicomd |
|- ( A e. V -> ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) ) |
18 |
1 17
|
e1a |
|- (. A e. V ->. ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) ). |
19 |
|
bitr3 |
|- ( ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) -> ( ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ) ) |
20 |
19
|
com12 |
|- ( ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> ( ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ) ) |
21 |
14 18 20
|
e11 |
|- (. A e. V ->. ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ). |
22 |
21
|
gen11 |
|- (. A e. V ->. A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ). |
23 |
|
abbi |
|- ( A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) <-> { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) |
24 |
23
|
biimpi |
|- ( A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) |
25 |
22 24
|
e1a |
|- (. A e. V ->. { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ). |
26 |
|
csbab |
|- [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } |
27 |
26
|
a1i |
|- ( A e. V -> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } ) |
28 |
1 27
|
e1a |
|- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } ). |
29 |
|
eqeq2 |
|- ( { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } <-> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) ) |
30 |
29
|
biimpd |
|- ( { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } -> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) ) |
31 |
25 28 30
|
e11 |
|- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ). |
32 |
|
dfrn3 |
|- ran B = { y | E. w <. w , y >. e. B } |
33 |
32
|
ax-gen |
|- A. x ran B = { y | E. w <. w , y >. e. B } |
34 |
|
csbeq2 |
|- ( A. x ran B = { y | E. w <. w , y >. e. B } -> [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ) |
35 |
34
|
a1i |
|- ( A e. V -> ( A. x ran B = { y | E. w <. w , y >. e. B } -> [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ) ) |
36 |
1 33 35
|
e10 |
|- (. A e. V ->. [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ). |
37 |
|
eqeq2 |
|- ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } <-> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) ) |
38 |
37
|
biimpd |
|- ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } -> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) ) |
39 |
31 36 38
|
e11 |
|- (. A e. V ->. [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ). |
40 |
|
dfrn3 |
|- ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B } |
41 |
|
eqeq2 |
|- ( ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = ran [_ A / x ]_ B <-> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) ) |
42 |
41
|
biimprcd |
|- ( [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> [_ A / x ]_ ran B = ran [_ A / x ]_ B ) ) |
43 |
39 40 42
|
e10 |
|- (. A e. V ->. [_ A / x ]_ ran B = ran [_ A / x ]_ B ). |
44 |
43
|
in1 |
|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B ) |