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