Step |
Hyp |
Ref |
Expression |
1 |
|
ral3xpf.1 |
|- F/ y ph |
2 |
|
ral3xpf.2 |
|- F/ z ph |
3 |
|
ral3xpf.3 |
|- F/ w ph |
4 |
|
ral3xpf.4 |
|- F/ x ps |
5 |
|
ral3xpf.5 |
|- ( x = <. <. y , z >. , w >. -> ( ph <-> ps ) ) |
6 |
|
df-ral |
|- ( A. x e. ( ( A X. B ) X. C ) ph <-> A. x ( x e. ( ( A X. B ) X. C ) -> ph ) ) |
7 |
1
|
r19.23 |
|- ( A. y e. A ( E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) <-> ( E. y e. A E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
8 |
3
|
r19.23 |
|- ( A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> ( E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
9 |
8
|
ralbii |
|- ( A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. z e. B ( E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
10 |
2
|
r19.23 |
|- ( A. z e. B ( E. w e. C x = <. <. y , z >. , w >. -> ph ) <-> ( E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
11 |
9 10
|
bitri |
|- ( A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> ( E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
12 |
11
|
ralbii |
|- ( A. y e. A A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. y e. A ( E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
13 |
|
elxpxp |
|- ( x e. ( ( A X. B ) X. C ) <-> E. y e. A E. z e. B E. w e. C x = <. <. y , z >. , w >. ) |
14 |
13
|
imbi1i |
|- ( ( x e. ( ( A X. B ) X. C ) -> ph ) <-> ( E. y e. A E. z e. B E. w e. C x = <. <. y , z >. , w >. -> ph ) ) |
15 |
7 12 14
|
3bitr4ri |
|- ( ( x e. ( ( A X. B ) X. C ) -> ph ) <-> A. y e. A A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) ) |
16 |
15
|
albii |
|- ( A. x ( x e. ( ( A X. B ) X. C ) -> ph ) <-> A. x A. y e. A A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) ) |
17 |
|
ralcom4 |
|- ( A. y e. A A. x A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. x A. y e. A A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) ) |
18 |
|
ralcom4 |
|- ( A. z e. B A. x A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. x A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) ) |
19 |
|
ralcom4 |
|- ( A. w e. C A. x ( x = <. <. y , z >. , w >. -> ph ) <-> A. x A. w e. C ( x = <. <. y , z >. , w >. -> ph ) ) |
20 |
|
opex |
|- <. <. y , z >. , w >. e. _V |
21 |
4 20 5
|
ceqsal |
|- ( A. x ( x = <. <. y , z >. , w >. -> ph ) <-> ps ) |
22 |
21
|
ralbii |
|- ( A. w e. C A. x ( x = <. <. y , z >. , w >. -> ph ) <-> A. w e. C ps ) |
23 |
19 22
|
bitr3i |
|- ( A. x A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. w e. C ps ) |
24 |
23
|
ralbii |
|- ( A. z e. B A. x A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. z e. B A. w e. C ps ) |
25 |
18 24
|
bitr3i |
|- ( A. x A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. z e. B A. w e. C ps ) |
26 |
25
|
ralbii |
|- ( A. y e. A A. x A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. y e. A A. z e. B A. w e. C ps ) |
27 |
17 26
|
bitr3i |
|- ( A. x A. y e. A A. z e. B A. w e. C ( x = <. <. y , z >. , w >. -> ph ) <-> A. y e. A A. z e. B A. w e. C ps ) |
28 |
6 16 27
|
3bitri |
|- ( A. x e. ( ( A X. B ) X. C ) ph <-> A. y e. A A. z e. B A. w e. C ps ) |