Description: Alternate version of s2dm , having a shorter proof, but requiring that A and B are sets. (Contributed by AV, 9-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | s2dmALT | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → dom ⟨“ 𝐴 𝐵 ”⟩ = { 0 , 1 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s2prop | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ⟨“ 𝐴 𝐵 ”⟩ = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) | |
| 2 | 1 | dmeqd | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → dom ⟨“ 𝐴 𝐵 ”⟩ = dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } ) |
| 3 | dmpropg | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → dom { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐵 ⟩ } = { 0 , 1 } ) | |
| 4 | 2 3 | eqtrd | ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → dom ⟨“ 𝐴 𝐵 ”⟩ = { 0 , 1 } ) |