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 bitrdi φ 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 bitrdi φ 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 χ