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

Metamath Proof Explorer

Theorem snopsuppss

Description: The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019)

		Ref	Expression
	Assertion	snopsuppss	$⊢ \{⟨X, Y⟩\} supp Z \subseteq \{X\}$

Proof

Step	Hyp	Ref	Expression
1		suppssdm	$⊢ \{⟨X, Y⟩\} supp Z \subseteq dom \{⟨X, Y⟩\}$
2		dmsnopss	$⊢ dom \{⟨X, Y⟩\} \subseteq \{X\}$
3	1 2	sstri	$⊢ \{⟨X, Y⟩\} supp Z \subseteq \{X\}$