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 ⊢Ⅎyφ
ralxp3f.2 ⊢Ⅎzφ
ralxp3f.3 ⊢Ⅎwφ
ralxp3f.4 ⊢Ⅎxψ
ralxp3f.5 ⊢x=yzw→φ↔ψ
Assertion ralxp3f ⊢∀x∈A×B×Cφ↔∀y∈A∀z∈B∀w∈Cψ

Proof

Step Hyp Ref Expression
1 ralxp3f.1 ⊢Ⅎyφ
2 ralxp3f.2 ⊢Ⅎzφ
3 ralxp3f.3 ⊢Ⅎwφ
4 ralxp3f.4 ⊢Ⅎxψ
5 ralxp3f.5 ⊢x=yzw→φ↔ψ
6 df-ral ⊢∀x∈A×B×Cφ↔∀xx∈A×B×C→φ
7 el2xptp ⊢x∈A×B×C↔∃y∈A∃z∈B∃w∈Cx=yzw
8 7 imbi1i ⊢x∈A×B×C→φ↔∃y∈A∃z∈B∃w∈Cx=yzw→φ
9 3 r19.23 ⊢∀w∈Cx=yzw→φ↔∃w∈Cx=yzw→φ
10 9 ralbii ⊢∀z∈B∀w∈Cx=yzw→φ↔∀z∈B∃w∈Cx=yzw→φ
11 2 r19.23 ⊢∀z∈B∃w∈Cx=yzw→φ↔∃z∈B∃w∈Cx=yzw→φ
12 10 11 bitri ⊢∀z∈B∀w∈Cx=yzw→φ↔∃z∈B∃w∈Cx=yzw→φ
13 12 ralbii ⊢∀y∈A∀z∈B∀w∈Cx=yzw→φ↔∀y∈A∃z∈B∃w∈Cx=yzw→φ
14 1 r19.23 ⊢∀y∈A∃z∈B∃w∈Cx=yzw→φ↔∃y∈A∃z∈B∃w∈Cx=yzw→φ
15 13 14 bitr2i ⊢∃y∈A∃z∈B∃w∈Cx=yzw→φ↔∀y∈A∀z∈B∀w∈Cx=yzw→φ
16 8 15 bitri ⊢x∈A×B×C→φ↔∀y∈A∀z∈B∀w∈Cx=yzw→φ
17 16 albii ⊢∀xx∈A×B×C→φ↔∀x∀y∈A∀z∈B∀w∈Cx=yzw→φ
18 ralcom4 ⊢∀y∈A∀x∀z∈B∀w∈Cx=yzw→φ↔∀x∀y∈A∀z∈B∀w∈Cx=yzw→φ
19 ralcom4 ⊢∀z∈B∀x∀w∈Cx=yzw→φ↔∀x∀z∈B∀w∈Cx=yzw→φ
20 ralcom4 ⊢∀w∈C∀xx=yzw→φ↔∀x∀w∈Cx=yzw→φ
21 otex ⊢yzw∈V
22 4 21 5 ceqsal ⊢∀xx=yzw→φ↔ψ
23 22 ralbii ⊢∀w∈C∀xx=yzw→φ↔∀w∈Cψ
24 20 23 bitr3i ⊢∀x∀w∈Cx=yzw→φ↔∀w∈Cψ
25 24 ralbii ⊢∀z∈B∀x∀w∈Cx=yzw→φ↔∀z∈B∀w∈Cψ
26 19 25 bitr3i ⊢∀x∀z∈B∀w∈Cx=yzw→φ↔∀z∈B∀w∈Cψ
27 26 ralbii ⊢∀y∈A∀x∀z∈B∀w∈Cx=yzw→φ↔∀y∈A∀z∈B∀w∈Cψ
28 18 27 bitr3i ⊢∀x∀y∈A∀z∈B∀w∈Cx=yzw→φ↔∀y∈A∀z∈B∀w∈Cψ
29 6 17 28 3bitri ⊢∀x∈A×B×Cφ↔∀y∈A∀z∈B∀w∈Cψ