Metamath Proof Explorer

Theorem ralxpxfr2d

Description: Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Hypotheses ralxpxfr2d.a ⊢ A ∈ V
ralxpxfr2d.b ⊢ φ → x ∈ B ↔ ∃ y ∈ C ∃ z ∈ D x = A
ralxpxfr2d.c ⊢ φ ∧ x = A → ψ ↔ χ
Assertion ralxpxfr2d ⊢ φ → ∀ x ∈ B ψ ↔ ∀ y ∈ C ∀ z ∈ D χ

Proof

Step Hyp Ref Expression
1 ralxpxfr2d.a ⊢ A ∈ V
2 ralxpxfr2d.b ⊢ φ → x ∈ B ↔ ∃ y ∈ C ∃ z ∈ D x = A
3 ralxpxfr2d.c ⊢ φ ∧ x = A → ψ ↔ χ
4 df-ral ⊢ ∀ x ∈ B ψ ↔ ∀ x x ∈ B → ψ
5 2 imbi1d ⊢ φ → x ∈ B → ψ ↔ ∃ y ∈ C ∃ z ∈ D x = A → ψ
6 5 albidv ⊢ φ → ∀ x x ∈ B → ψ ↔ ∀ x ∃ y ∈ C ∃ z ∈ D x = A → ψ
7 4 6 syl5bb ⊢ φ → ∀ x ∈ B ψ ↔ ∀ x ∃ y ∈ C ∃ z ∈ D x = A → ψ
8 ralcom4 ⊢ ∀ y ∈ C ∀ x ∀ z ∈ D x = A → ψ ↔ ∀ x ∀ y ∈ C ∀ z ∈ D x = A → ψ
9 ralcom4 ⊢ ∀ z ∈ D ∀ x x = A → ψ ↔ ∀ x ∀ z ∈ D x = A → ψ
10 9 ralbii ⊢ ∀ y ∈ C ∀ z ∈ D ∀ x x = A → ψ ↔ ∀ y ∈ C ∀ x ∀ z ∈ D x = A → ψ
11 r19.23v ⊢ ∀ z ∈ D x = A → ψ ↔ ∃ z ∈ D x = A → ψ
12 11 ralbii ⊢ ∀ y ∈ C ∀ z ∈ D x = A → ψ ↔ ∀ y ∈ C ∃ z ∈ D x = A → ψ
13 r19.23v ⊢ ∀ y ∈ C ∃ z ∈ D x = A → ψ ↔ ∃ y ∈ C ∃ z ∈ D x = A → ψ
14 12 13 bitr2i ⊢ ∃ y ∈ C ∃ z ∈ D x = A → ψ ↔ ∀ y ∈ C ∀ z ∈ D x = A → ψ
15 14 albii ⊢ ∀ x ∃ y ∈ C ∃ z ∈ D x = A → ψ ↔ ∀ x ∀ y ∈ C ∀ z ∈ D x = A → ψ
16 8 10 15 3bitr4ri ⊢ ∀ x ∃ y ∈ C ∃ z ∈ D x = A → ψ ↔ ∀ y ∈ C ∀ z ∈ D ∀ x x = A → ψ
17 7 16 syl6bb ⊢ φ → ∀ x ∈ B ψ ↔ ∀ y ∈ C ∀ z ∈ D ∀ x x = A → ψ
18 3 pm5.74da ⊢ φ → x = A → ψ ↔ x = A → χ
19 18 albidv ⊢ φ → ∀ x x = A → ψ ↔ ∀ x x = A → χ
20 biidd ⊢ x = A → χ ↔ χ
21 1 20 ceqsalv ⊢ ∀ x x = A → χ ↔ χ
22 19 21 syl6bb ⊢ φ → ∀ x x = A → ψ ↔ χ
23 22 2ralbidv ⊢ φ → ∀ y ∈ C ∀ z ∈ D ∀ x x = A → ψ ↔ ∀ y ∈ C ∀ z ∈ D χ
24 17 23 bitrd ⊢ φ → ∀ x ∈ B ψ ↔ ∀ y ∈ C ∀ z ∈ D χ