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
⊢ A = B
raleqbii.2
⊢ ψ ↔ χ
Assertion
raleqbii
⊢ ∀ x ∈ A ψ ↔ ∀ x ∈ B χ
Proof
Step
Hyp
Ref
Expression
1
raleqbii.1
⊢ A = B
2
raleqbii.2
⊢ ψ ↔ χ
3
1
eleq2i
⊢ x ∈ A ↔ x ∈ B
4
3 2
imbi12i
⊢ x ∈ A → ψ ↔ x ∈ B → χ
5
4
ralbii2
⊢ ∀ x ∈ A ψ ↔ ∀ x ∈ B χ