Description: Alternate version of s1dm , having a shorter proof, but requiring that A is a set. (Contributed by AV, 9-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | s1dmALT | |- ( A e. S -> dom <" A "> = { 0 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1val | |- ( A e. S -> <" A "> = { <. 0 , A >. } ) |
|
2 | 1 | dmeqd | |- ( A e. S -> dom <" A "> = dom { <. 0 , A >. } ) |
3 | dmsnopg | |- ( A e. S -> dom { <. 0 , A >. } = { 0 } ) |
|
4 | 2 3 | eqtrd | |- ( A e. S -> dom <" A "> = { 0 } ) |