Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Classes without the axiom of extensionality
bj-issettru
Next ⟩
bj-elabtru
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-issettru
Description:
Weak version of
isset
without
ax-ext
.
(Contributed by
BJ
, 24-Apr-2024)
Ref
Expression
Assertion
bj-issettru
⊢
∃
x
x
=
A
↔
A
∈
y
|
⊤
Proof
Step
Hyp
Ref
Expression
1
bj-denotes
⊢
∃
x
x
=
A
↔
∃
z
z
=
A
2
bj-denoteslem
⊢
∃
z
z
=
A
↔
A
∈
y
|
⊤
3
1
2
bitri
⊢
∃
x
x
=
A
↔
A
∈
y
|
⊤