Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
domrefg
Next ⟩
en2d
Metamath Proof Explorer
Ascii
Structured
Theorem
domrefg
Description:
Dominance is reflexive.
(Contributed by
NM
, 18-Jun-1998)
Ref
Expression
Assertion
domrefg
⊢
(
𝐴
∈
𝑉
→
𝐴
≼
𝐴
)
Proof
Step
Hyp
Ref
Expression
1
enrefg
⊢
(
𝐴
∈
𝑉
→
𝐴
≈
𝐴
)
2
endom
⊢
(
𝐴
≈
𝐴
→
𝐴
≼
𝐴
)
3
1
2
syl
⊢
(
𝐴
∈
𝑉
→
𝐴
≼
𝐴
)