Metamath Proof Explorer


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