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

Metamath Proof Explorer

Theorem ralxfr2d

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by Mario Carneiro, 20-Aug-2014)

Ref Expression
Hypotheses ralxfr2d.1 ⊢ φ ∧ y ∈ C → A ∈ V
ralxfr2d.2 ⊢ φ → x ∈ B ↔ ∃ y ∈ C x = A
ralxfr2d.3 ⊢ φ ∧ x = A → ψ ↔ χ
Assertion ralxfr2d ⊢ φ → ∀ x ∈ B ψ ↔ ∀ y ∈ C χ

Proof

Step Hyp Ref Expression
1 ralxfr2d.1 ⊢ φ ∧ y ∈ C → A ∈ V
2 ralxfr2d.2 ⊢ φ → x ∈ B ↔ ∃ y ∈ C x = A
3 ralxfr2d.3 ⊢ φ ∧ x = A → ψ ↔ χ
4 elisset ⊢ A ∈ V → ∃ x x = A
5 1 4 syl ⊢ φ ∧ y ∈ C → ∃ x x = A
6 2 biimprd ⊢ φ → ∃ y ∈ C x = A → x ∈ B
7 r19.23v ⊢ ∀ y ∈ C x = A → x ∈ B ↔ ∃ y ∈ C x = A → x ∈ B
8 6 7 sylibr ⊢ φ → ∀ y ∈ C x = A → x ∈ B
9 8 r19.21bi ⊢ φ ∧ y ∈ C → x = A → x ∈ B
10 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
11 9 10 mpbidi ⊢ φ ∧ y ∈ C → x = A → A ∈ B
12 11 exlimdv ⊢ φ ∧ y ∈ C → ∃ x x = A → A ∈ B
13 5 12 mpd ⊢ φ ∧ y ∈ C → A ∈ B
14 2 biimpa ⊢ φ ∧ x ∈ B → ∃ y ∈ C x = A
15 13 14 3 ralxfrd ⊢ φ → ∀ x ∈ B ψ ↔ ∀ y ∈ C χ