This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvraldva2

Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses cbvraldva2.1 ⊢ φ ∧ x = y → ψ ↔ χ
cbvraldva2.2 ⊢ φ ∧ x = y → A = B
Assertion cbvraldva2 ⊢ φ → ∀ 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 imbi12d ⊢ φ ∧ x = y → x ∈ A → ψ ↔ y ∈ B → χ
6 5 expcom ⊢ x = y → φ → x ∈ A → ψ ↔ y ∈ B → χ
7 6 pm5.74d ⊢ x = y → φ → x ∈ A → ψ ↔ φ → y ∈ B → χ
8 7 cbvalvw ⊢ ∀ x φ → x ∈ A → ψ ↔ ∀ y φ → y ∈ B → χ
9 19.21v ⊢ ∀ x φ → x ∈ A → ψ ↔ φ → ∀ x x ∈ A → ψ
10 19.21v ⊢ ∀ y φ → y ∈ B → χ ↔ φ → ∀ y y ∈ B → χ
11 8 9 10 3bitr3i ⊢ φ → ∀ x x ∈ A → ψ ↔ φ → ∀ y y ∈ B → χ
12 11 pm5.74ri ⊢ φ → ∀ x x ∈ A → ψ ↔ ∀ y y ∈ B → χ
13 df-ral ⊢ ∀ x ∈ A ψ ↔ ∀ x x ∈ A → ψ
14 df-ral ⊢ ∀ y ∈ B χ ↔ ∀ y y ∈ B → χ
15 12 13 14 3bitr4g ⊢ φ → ∀ x ∈ A ψ ↔ ∀ y ∈ B χ