Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
enpr1g
Next ⟩
en1
Metamath Proof Explorer
Ascii
Unicode
Theorem
enpr1g
Description:
{ A , A }
has only one element.
(Contributed by
FL
, 15-Feb-2010)
Ref
Expression
Assertion
enpr1g
⊢
A
∈
V
→
A
A
≈
1
𝑜
Proof
Step
Hyp
Ref
Expression
1
dfsn2
⊢
A
=
A
A
2
ensn1g
⊢
A
∈
V
→
A
≈
1
𝑜
3
1
2
eqbrtrrid
⊢
A
∈
V
→
A
A
≈
1
𝑜