Theorem dmsnopss

Description: The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B ). (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	dmsnopss	⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		dmsnopg	⊢ ( 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
2		eqimss	⊢ ( dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
3	1 2	syl	⊢ ( 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
4		opprc2	⊢ ( ¬ 𝐵 ∈ V → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
5	4	sneqd	⊢ ( ¬ 𝐵 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = { ∅ } )
6	5	dmeqd	⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = dom { ∅ } )
7		dmsn0	⊢ dom { ∅ } = ∅
8	6 7	syl6eq	⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ )
9		0ss	⊢ ∅ ⊆ { 𝐴 }
10	8 9	eqsstrdi	⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
11	3 10	pm2.61i	⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }