Metamath Proof Explorer


Theorem cbvrexdva2

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 12-Aug-2023)

Ref Expression
Hypotheses cbvraldva2.1 φ x = y ψ χ
cbvraldva2.2 φ x = y A = B
Assertion cbvrexdva2 φ x A ψ y B χ

Proof

Step Hyp Ref Expression
1 cbvraldva2.1 φ x = y ψ χ
2 cbvraldva2.2 φ x = y A = B
3 simpr φ x = y x = y
4 3 2 eleq12d φ x = y x A y B
5 4 1 anbi12d φ x = y x A ψ y B χ
6 5 ancoms x = y φ x A ψ y B χ
7 6 pm5.32da x = y φ x A ψ φ y B χ
8 7 cbvexvw x φ x A ψ y φ y B χ
9 19.42v x φ x A ψ φ x x A ψ
10 19.42v y φ y B χ φ y y B χ
11 8 9 10 3bitr3i φ x x A ψ φ y y B χ
12 pm5.32 φ x x A ψ y y B χ φ x x A ψ φ y y B χ
13 11 12 mpbir φ x x A ψ y y B χ
14 df-rex x A ψ x x A ψ
15 df-rex y B χ y y B χ
16 13 14 15 3bitr4g φ x A ψ y B χ