Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-sngleq
Next ⟩
bj-elsngl
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-sngleq
Description:
Substitution property for
sngl
.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-sngleq
⊢
A
=
B
→
sngl
A
=
sngl
B
Proof
Step
Hyp
Ref
Expression
1
rexeq
⊢
A
=
B
→
∃
y
∈
A
x
=
y
↔
∃
y
∈
B
x
=
y
2
1
abbidv
⊢
A
=
B
→
x
|
∃
y
∈
A
x
=
y
=
x
|
∃
y
∈
B
x
=
y
3
df-bj-sngl
⊢
sngl
A
=
x
|
∃
y
∈
A
x
=
y
4
df-bj-sngl
⊢
sngl
B
=
x
|
∃
y
∈
B
x
=
y
5
2
3
4
3eqtr4g
⊢
A
=
B
→
sngl
A
=
sngl
B