Metamath Proof Explorer


Theorem ralxp3f

Description: Restricted for all over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses ral3xpf.1
|- F/ y ph
ral3xpf.2
|- F/ z ph
ral3xpf.3
|- F/ w ph
ral3xpf.4
|- F/ x ps
ral3xpf.5
|- ( x = <. <. y , z >. , w >. -> ( ph <-> ps ) )
Assertion ralxp3f
|- ( A. x e. ( ( A X. B ) X. C ) ph <-> A. y e. A A. z e. B A. w e. C ps )

Proof

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 )