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	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmsnopg	$$⊢B\in \mathrm{V}\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
2		eqimss	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}\to \mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$
3	1 2	syl	$$⊢B\in \mathrm{V}\to \mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$
4		opprc2	$$⊢\neg B\in \mathrm{V}\to ⟨A,B⟩=\varnothing$$
5	4	sneqd	$$⊢\neg B\in \mathrm{V}\to \left\{⟨A,B⟩\right\}=\left\{\varnothing \right\}$$
6	5	dmeqd	$$⊢\neg B\in \mathrm{V}\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\mathrm{dom}\left\{\varnothing \right\}$$
7		dmsn0	$$⊢\mathrm{dom}\left\{\varnothing \right\}=\varnothing$$
8	6 7	syl6eq	$$⊢\neg B\in \mathrm{V}\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\varnothing$$
9		0ss	$$⊢\varnothing \subseteq \left\{A\right\}$$
10	8 9	eqsstrdi	$$⊢\neg B\in \mathrm{V}\to \mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$
11	3 10	pm2.61i	$$⊢\mathrm{dom}\left\{⟨A,B⟩\right\}\subseteq \left\{A\right\}$$