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∈Dx=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∈Dx=A
3 ralxpxfr2d.c ⊢φ∧x=A→ψ↔χ
4 df-ral ⊢∀x∈Bψ↔∀xx∈B→ψ
5 2 imbi1d ⊢φ→x∈B→ψ↔∃y∈C∃z∈Dx=A→ψ
6 5 albidv ⊢φ→∀xx∈B→ψ↔∀x∃y∈C∃z∈Dx=A→ψ
7 4 6 bitrid ⊢φ→∀x∈Bψ↔∀x∃y∈C∃z∈Dx=A→ψ
8 ralcom4 ⊢∀y∈C∀x∀z∈Dx=A→ψ↔∀x∀y∈C∀z∈Dx=A→ψ
9 ralcom4 ⊢∀z∈D∀xx=A→ψ↔∀x∀z∈Dx=A→ψ
10 9 ralbii ⊢∀y∈C∀z∈D∀xx=A→ψ↔∀y∈C∀x∀z∈Dx=A→ψ
11 r19.23v ⊢∀z∈Dx=A→ψ↔∃z∈Dx=A→ψ
12 11 ralbii ⊢∀y∈C∀z∈Dx=A→ψ↔∀y∈C∃z∈Dx=A→ψ
13 r19.23v ⊢∀y∈C∃z∈Dx=A→ψ↔∃y∈C∃z∈Dx=A→ψ
14 12 13 bitr2i ⊢∃y∈C∃z∈Dx=A→ψ↔∀y∈C∀z∈Dx=A→ψ
15 14 albii ⊢∀x∃y∈C∃z∈Dx=A→ψ↔∀x∀y∈C∀z∈Dx=A→ψ
16 8 10 15 3bitr4ri ⊢∀x∃y∈C∃z∈Dx=A→ψ↔∀y∈C∀z∈D∀xx=A→ψ
17 7 16 bitrdi ⊢φ→∀x∈Bψ↔∀y∈C∀z∈D∀xx=A→ψ
18 3 pm5.74da ⊢φ→x=A→ψ↔x=A→χ
19 18 albidv ⊢φ→∀xx=A→ψ↔∀xx=A→χ
20 biidd ⊢x=A→χ↔χ
21 1 20 ceqsalv ⊢∀xx=A→χ↔χ
22 19 21 bitrdi ⊢φ→∀xx=A→ψ↔χ
23 22 2ralbidv ⊢φ→∀y∈C∀z∈D∀xx=A→ψ↔∀y∈C∀z∈Dχ
24 17 23 bitrd ⊢φ→∀x∈Bψ↔∀y∈C∀z∈Dχ