Theorem raleqi

Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypothesis	raleq1i.1	⊢ 𝐴 = 𝐵
Assertion	raleqi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		raleq1i.1	⊢ 𝐴 = 𝐵
2		raleq	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 ) )
3	1 2	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 )