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 χ