This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification raleleq
Description: All elements of a class are elements of a class equal to this class.
(Contributed by AV , 30-Oct-2020) (Proof shortened by Wolf Lammen , 18-Jul-2025)
Ref
Expression
Assertion
raleleq ⊢ A = B → ∀ x ∈ A x ∈ B
Proof
Step
Hyp
Ref
Expression
1
ralel ⊢ ∀ x ∈ B x ∈ B
2
raleq ⊢ A = B → ∀ x ∈ A x ∈ B ↔ ∀ x ∈ B x ∈ B
3
1 2
mpbiri ⊢ A = B → ∀ x ∈ A x ∈ B