Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
raleqbii
Metamath Proof Explorer
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
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜒 )