Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
ralel
Next ⟩
rgenw
Metamath Proof Explorer
Ascii
Unicode
Theorem
ralel
Description:
All elements of a class are elements of the class.
(Contributed by
AV
, 30-Oct-2020)
Ref
Expression
Assertion
ralel
⊢
∀
x
∈
A
x
∈
A
Proof
Step
Hyp
Ref
Expression
1
id
⊢
x
∈
A
→
x
∈
A
2
1
rgen
⊢
∀
x
∈
A
x
∈
A