Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
sdomdom
Next ⟩
sdomnen
Metamath Proof Explorer
Ascii
Unicode
Theorem
sdomdom
Description:
Strict dominance implies dominance.
(Contributed by
NM
, 10-Jun-1998)
Ref
Expression
Assertion
sdomdom
⊢
A
≺
B
→
A
≼
B
Proof
Step
Hyp
Ref
Expression
1
brsdom
⊢
A
≺
B
↔
A
≼
B
∧
¬
A
≈
B
2
1
simplbi
⊢
A
≺
B
→
A
≼
B