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