Theorem ralbi12f

Description: Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018)

	Ref	Expression
Hypotheses	ralbi12f.1	⊢ Ⅎ 𝑥 𝐴
	ralbi12f.2	⊢ Ⅎ 𝑥 𝐵
Assertion	ralbi12f	⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ralbi12f.1	⊢ Ⅎ 𝑥 𝐴
2		ralbi12f.2	⊢ Ⅎ 𝑥 𝐵
3		ralbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
4	1 2	raleqf	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
5	3 4	sylan9bbr	⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )