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

Metamath Proof Explorer

Theorem alxfr

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by NM, 18-Feb-2007)

Ref Expression
Hypothesis alxfr.1 ⊢ x = A → φ ↔ ψ
Assertion alxfr ⊢ ∀ y A ∈ B ∧ ∀ x ∃ y x = A → ∀ x φ ↔ ∀ y ψ

Proof

Step Hyp Ref Expression
1 alxfr.1 ⊢ x = A → φ ↔ ψ
2 1 spcgv ⊢ A ∈ B → ∀ x φ → ψ
3 2 com12 ⊢ ∀ x φ → A ∈ B → ψ
4 3 alimdv ⊢ ∀ x φ → ∀ y A ∈ B → ∀ y ψ
5 4 com12 ⊢ ∀ y A ∈ B → ∀ x φ → ∀ y ψ
6 5 adantr ⊢ ∀ y A ∈ B ∧ ∀ x ∃ y x = A → ∀ x φ → ∀ y ψ
7 nfa1 ⊢ Ⅎ y ∀ y ψ
8 nfv ⊢ Ⅎ y φ
9 sp ⊢ ∀ y ψ → ψ
10 9 1 syl5ibrcom ⊢ ∀ y ψ → x = A → φ
11 7 8 10 exlimd ⊢ ∀ y ψ → ∃ y x = A → φ
12 11 alimdv ⊢ ∀ y ψ → ∀ x ∃ y x = A → ∀ x φ
13 12 com12 ⊢ ∀ x ∃ y x = A → ∀ y ψ → ∀ x φ
14 13 adantl ⊢ ∀ y A ∈ B ∧ ∀ x ∃ y x = A → ∀ y ψ → ∀ x φ
15 6 14 impbid ⊢ ∀ y A ∈ B ∧ ∀ x ∃ y x = A → ∀ x φ ↔ ∀ y ψ