Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-clex
Next ⟩
bj-csngl
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-clex
Description:
Sethood of certain classes.
(Contributed by
BJ
, 2-Apr-2019)
Ref
Expression
Assertion
bj-clex
⊢
A
∈
V
→
x
|
x
∈
A
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
imaexg
⊢
A
∈
V
→
A
B
∈
V
2
bj-snsetex
⊢
A
B
∈
V
→
x
|
x
∈
A
B
∈
V
3
1
2
syl
⊢
A
∈
V
→
x
|
x
∈
A
B
∈
V