This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \{⟨A, B⟩\} \subseteq \{A\}$

Proof

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