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 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion alxfr ( ( ∀ 𝑦 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )

Proof

Step Hyp Ref Expression
1 alxfr.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 1 spcgv ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → 𝜓 ) )
3 2 com12 ⊢ ( ∀ 𝑥 𝜑 → ( 𝐴 ∈ 𝐵 → 𝜓 ) )
4 3 alimdv ⊢ ( ∀ 𝑥 𝜑 → ( ∀ 𝑦 𝐴 ∈ 𝐵 → ∀ 𝑦 𝜓 ) )
5 4 com12 ⊢ ( ∀ 𝑦 𝐴 ∈ 𝐵 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
6 5 adantr ⊢ ( ( ∀ 𝑦 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
7 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 𝜓
8 nfv ⊢ Ⅎ 𝑦 𝜑
9 sp ⊢ ( ∀ 𝑦 𝜓 → 𝜓 )
10 9 1 syl5ibrcom ⊢ ( ∀ 𝑦 𝜓 → ( 𝑥 = 𝐴 → 𝜑 ) )
11 7 8 10 exlimd ⊢ ( ∀ 𝑦 𝜓 → ( ∃ 𝑦 𝑥 = 𝐴 → 𝜑 ) )
12 11 alimdv ⊢ ( ∀ 𝑦 𝜓 → ( ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 → ∀ 𝑥 𝜑 ) )
13 12 com12 ⊢ ( ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 ) )
14 13 adantl ⊢ ( ( ∀ 𝑦 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 ) → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 ) )
15 6 14 impbid ⊢ ( ( ∀ 𝑦 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∃ 𝑦 𝑥 = 𝐴 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )