Metamath Proof Explorer


Theorem raleqbii

Description: Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 raleqbii.1 𝐴 = 𝐵
2 raleqbii.2 ( 𝜓𝜒 )
3 1 eleq2i ( 𝑥𝐴𝑥𝐵 )
4 3 2 imbi12i ( ( 𝑥𝐴𝜓 ) ↔ ( 𝑥𝐵𝜒 ) )
5 4 ralbii2 ( ∀ 𝑥𝐴 𝜓 ↔ ∀ 𝑥𝐵 𝜒 )