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 | ⊢ ( 𝐴 ∈ 𝑆 → dom 〈“ 𝐴 ”〉 = { 0 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s1val | ⊢ ( 𝐴 ∈ 𝑆 → 〈“ 𝐴 ”〉 = { 〈 0 , 𝐴 〉 } ) | |
2 | 1 | dmeqd | ⊢ ( 𝐴 ∈ 𝑆 → dom 〈“ 𝐴 ”〉 = dom { 〈 0 , 𝐴 〉 } ) |
3 | dmsnopg | ⊢ ( 𝐴 ∈ 𝑆 → dom { 〈 0 , 𝐴 〉 } = { 0 } ) | |
4 | 2 3 | eqtrd | ⊢ ( 𝐴 ∈ 𝑆 → dom 〈“ 𝐴 ”〉 = { 0 } ) |