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