Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Classes without the axiom of extensionality
bj-denoteslem
Next ⟩
bj-denotes
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-denoteslem
Description:
Lemma for
bj-denotes
.
(Contributed by
BJ
, 24-Apr-2024)
Ref
Expression
Assertion
bj-denoteslem
⊢
∃
x
x
=
A
↔
A
∈
y
|
⊤
Proof
Step
Hyp
Ref
Expression
1
vextru
⊢
x
∈
y
|
⊤
2
1
biantru
⊢
x
=
A
↔
x
=
A
∧
x
∈
y
|
⊤
3
2
exbii
⊢
∃
x
x
=
A
↔
∃
x
x
=
A
∧
x
∈
y
|
⊤
4
dfclel
⊢
A
∈
y
|
⊤
↔
∃
x
x
=
A
∧
x
∈
y
|
⊤
5
3
4
bitr4i
⊢
∃
x
x
=
A
↔
A
∈
y
|
⊤