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