This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralxp3f

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

Ref Expression
Hypotheses ralxp3f.1 
|- F/ y ph
ralxp3f.2 
|- F/ z ph
ralxp3f.3 
|- F/ w ph
ralxp3f.4 
|- F/ x ps
ralxp3f.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 ralxp3f.1 
 |-  F/ y ph
2 ralxp3f.2 
 |-  F/ z ph
3 ralxp3f.3 
 |-  F/ w ph
4 ralxp3f.4 
 |-  F/ x ps
5 ralxp3f.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 el2xptp 
 |-  ( x e. ( ( A X. B ) X. C ) <-> E. y e. A E. z e. B E. w e. C x = <. y , z , w >. )
8 7 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 ) )
9 3 r19.23 
 |-  ( A. w e. C ( x = <. y , z , w >. -> ph ) <-> ( E. w e. C x = <. y , z , w >. -> ph ) )
10 9 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 ) )
11 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 ) )
12 10 11 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 ) )
13 12 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 ) )
14 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 ) )
15 13 14 bitr2i 
 |-  ( ( E. y e. A E. z e. B E. w e. C x = <. y , z , w >. -> ph ) <-> A. y e. A A. z e. B A. w e. C ( x = <. y , z , w >. -> ph ) )
16 8 15 bitri 
 |-  ( ( 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 ) )
17 16 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 ) )
18 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 ) )
19 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 ) )
20 ralcom4 
 |-  ( A. w e. C A. x ( x = <. y , z , w >. -> ph ) <-> A. x A. w e. C ( x = <. y , z , w >. -> ph ) )
21 otex 
 |-  <. y , z , w >. e. _V
22 4 21 5 ceqsal 
 |-  ( A. x ( x = <. y , z , w >. -> ph ) <-> ps )
23 22 ralbii 
 |-  ( A. w e. C A. x ( x = <. y , z , w >. -> ph ) <-> A. w e. C ps )
24 20 23 bitr3i 
 |-  ( A. x A. w e. C ( x = <. y , z , w >. -> ph ) <-> A. w e. C ps )
25 24 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 )
26 19 25 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 )
27 26 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 )
28 18 27 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 )
29 6 17 28 3bitri 
 |-  ( A. x e. ( ( A X. B ) X. C ) ph <-> A. y e. A A. z e. B A. w e. C ps )