Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. A e. V ->. A e. V ). |
2 |
|
sbcel12 |
|- ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) |
3 |
2
|
a1i |
|- ( A e. V -> ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ) |
4 |
1 3
|
e1a |
|- (. A e. V ->. ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ). |
5 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ w = w ) |
6 |
1 5
|
e1a |
|- (. A e. V ->. [_ A / x ]_ w = w ). |
7 |
|
eleq1 |
|- ( [_ A / x ]_ w = w -> ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ) |
8 |
6 7
|
e1a |
|- (. A e. V ->. ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ). |
9 |
|
bibi1 |
|- ( ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) -> ( ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) <-> ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ) ) |
10 |
9
|
biimprd |
|- ( ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) -> ( ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) -> ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ) ) |
11 |
4 8 10
|
e11 |
|- (. A e. V ->. ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ). |
12 |
|
sbcel12 |
|- ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) |
13 |
12
|
a1i |
|- ( A e. V -> ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ) |
14 |
1 13
|
e1a |
|- (. A e. V ->. ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ). |
15 |
|
csbconstg |
|- ( A e. V -> [_ A / x ]_ y = y ) |
16 |
1 15
|
e1a |
|- (. A e. V ->. [_ A / x ]_ y = y ). |
17 |
|
eleq1 |
|- ( [_ A / x ]_ y = y -> ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ) |
18 |
16 17
|
e1a |
|- (. A e. V ->. ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ). |
19 |
|
bibi1 |
|- ( ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) -> ( ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) <-> ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ) ) |
20 |
19
|
biimprd |
|- ( ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) -> ( ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) -> ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ) ) |
21 |
14 18 20
|
e11 |
|- (. A e. V ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ). |
22 |
|
pm4.38 |
|- ( ( ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) /\ ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ) -> ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) |
23 |
22
|
ex |
|- ( ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) -> ( ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) -> ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
24 |
11 21 23
|
e11 |
|- (. A e. V ->. ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ). |
25 |
|
sbcan |
|- ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) |
26 |
25
|
a1i |
|- ( A e. V -> ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ) |
27 |
1 26
|
e1a |
|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ). |
28 |
|
bibi1 |
|- ( ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) -> ( ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) <-> ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
29 |
28
|
biimprcd |
|- ( ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) -> ( ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) -> ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
30 |
24 27 29
|
e11 |
|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ). |
31 |
|
sbcg |
|- ( A e. V -> ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) ) |
32 |
1 31
|
e1a |
|- (. A e. V ->. ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) ). |
33 |
|
pm4.38 |
|- ( ( ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) /\ ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
34 |
33
|
expcom |
|- ( ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) -> ( ( [. A / x ]. z = <. w , y >. <-> z = <. w , y >. ) -> ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
35 |
30 32 34
|
e11 |
|- (. A e. V ->. ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
36 |
|
sbcan |
|- ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) |
37 |
36
|
a1i |
|- ( A e. V -> ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ) |
38 |
1 37
|
e1a |
|- (. A e. V ->. ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ). |
39 |
|
bibi1 |
|- ( ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) -> ( ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) <-> ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
40 |
39
|
biimprcd |
|- ( ( ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) -> ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
41 |
35 38 40
|
e11 |
|- (. A e. V ->. ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
42 |
41
|
gen11 |
|- (. A e. V ->. A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
43 |
|
exbi |
|- ( A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
44 |
42 43
|
e1a |
|- (. A e. V ->. ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
45 |
|
sbcex2 |
|- ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) |
46 |
45
|
a1i |
|- ( A e. V -> ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ) |
47 |
1 46
|
e1a |
|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ). |
48 |
|
bibi1 |
|- ( ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) -> ( ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) <-> ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
49 |
48
|
biimprcd |
|- ( ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) -> ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
50 |
44 47 49
|
e11 |
|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
51 |
50
|
gen11 |
|- (. A e. V ->. A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
52 |
|
exbi |
|- ( A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) |
53 |
51 52
|
e1a |
|- (. A e. V ->. ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
54 |
|
sbcex2 |
|- ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) |
55 |
54
|
a1i |
|- ( A e. V -> ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ) |
56 |
1 55
|
e1a |
|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ). |
57 |
|
bibi1 |
|- ( ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) -> ( ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) <-> ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
58 |
57
|
biimprcd |
|- ( ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> ( ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) -> ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ) ) |
59 |
53 56 58
|
e11 |
|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
60 |
59
|
gen11 |
|- (. A e. V ->. A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). |
61 |
|
abbi |
|- ( A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) <-> { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) |
62 |
61
|
biimpi |
|- ( A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) -> { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) |
63 |
60 62
|
e1a |
|- (. A e. V ->. { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). |
64 |
|
csbab |
|- [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } |
65 |
64
|
a1i |
|- ( A e. V -> [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ) |
66 |
1 65
|
e1a |
|- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ). |
67 |
|
eqeq2 |
|- ( { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } <-> [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) ) |
68 |
67
|
biimpd |
|- ( { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } -> [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) ) |
69 |
63 66 68
|
e11 |
|- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). |
70 |
|
df-xp |
|- ( B X. C ) = { <. w , y >. | ( w e. B /\ y e. C ) } |
71 |
|
df-opab |
|- { <. w , y >. | ( w e. B /\ y e. C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } |
72 |
70 71
|
eqtri |
|- ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } |
73 |
72
|
ax-gen |
|- A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } |
74 |
|
csbeq2 |
|- ( A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } -> [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ) |
75 |
74
|
a1i |
|- ( A e. V -> ( A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } -> [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ) ) |
76 |
1 73 75
|
e10 |
|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ). |
77 |
|
eqeq2 |
|- ( [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } <-> [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) ) |
78 |
77
|
biimpd |
|- ( [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } -> [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) ) |
79 |
69 76 78
|
e11 |
|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). |
80 |
|
df-xp |
|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } |
81 |
|
df-opab |
|- { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } |
82 |
80 81
|
eqtri |
|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } |
83 |
|
eqeq2 |
|- ( ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) <-> [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ) ) |
84 |
83
|
biimprcd |
|- ( [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> ( ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ) ) |
85 |
79 82 84
|
e10 |
|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ). |
86 |
85
|
in1 |
|- ( A e. V -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ) |