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 ⊢ 𝐴 ∈ V
ralxpxfr2d.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 ) )
ralxpxfr2d.c ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion ralxpxfr2d ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 𝜒 ) )

Proof

Step Hyp Ref Expression
1 ralxpxfr2d.a ⊢ 𝐴 ∈ V
2 ralxpxfr2d.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 ) )
3 ralxpxfr2d.c ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) )
5 2 imbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 → 𝜓 ) ↔ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ) )
6 5 albidv ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜓 ) ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ) )
7 4 6 bitrid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ) )
8 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) )
9 ralcom4 ⊢ ( ∀ 𝑧 ∈ 𝐷 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) )
10 9 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) )
11 r19.23v ⊢ ( ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) )
12 11 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ∈ 𝐶 ( ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) )
13 r19.23v ⊢ ( ∀ 𝑦 ∈ 𝐶 ( ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) )
14 12 13 bitr2i ⊢ ( ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) )
15 14 albii ⊢ ( ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ( 𝑥 = 𝐴 → 𝜓 ) )
16 8 10 15 3bitr4ri ⊢ ( ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) )
17 7 16 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) )
18 3 pm5.74da ⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( 𝑥 = 𝐴 → 𝜒 ) ) )
19 18 albidv ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜒 ) ) )
20 biidd ⊢ ( 𝑥 = 𝐴 → ( 𝜒 ↔ 𝜒 ) )
21 1 20 ceqsalv ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜒 ) ↔ 𝜒 )
22 19 21 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜒 ) )
23 22 2ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 𝜒 ) )
24 17 23 bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐷 𝜒 ) )