Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
raleleqOLD
Metamath Proof Explorer
Description: Obsolete version of raleleq as of 18-Jul-2025. (Contributed by AV , 30-Oct-2020) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
raleleqOLD
⊢ A = B → ∀ x ∈ A x ∈ B
Proof
Step
Hyp
Ref
Expression
1
ralel
⊢ ∀ x ∈ B x ∈ B
2
id
⊢ A = B → A = B
3
2
raleqdv
⊢ A = B → ∀ x ∈ A x ∈ B ↔ ∀ x ∈ B x ∈ B
4
1 3
mpbiri
⊢ A = B → ∀ x ∈ A x ∈ B