Metamath Proof Explorer


Theorem raleqbidv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007) Remove usage of ax-10 , ax-11 , and ax-12 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023)

Ref Expression
Hypotheses raleqbidv.1 ( 𝜑𝐴 = 𝐵 )
raleqbidv.2 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion raleqbidv ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥𝐵 𝜒 ) )

Proof

Step Hyp Ref Expression
1 raleqbidv.1 ( 𝜑𝐴 = 𝐵 )
2 raleqbidv.2 ( 𝜑 → ( 𝜓𝜒 ) )
3 1 eleq2d ( 𝜑 → ( 𝑥𝐴𝑥𝐵 ) )
4 3 2 imbi12d ( 𝜑 → ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) ) )
5 4 ralbidv2 ( 𝜑 → ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥𝐵 𝜒 ) )