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 ( 𝜑 → ( ∀ 𝑥𝐵 𝜓 ↔ ∀ 𝑦𝐶𝑧𝐷 𝜒 ) )