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	⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ { 𝑋 }

Proof

Step	Hyp	Ref	Expression
1		suppssdm	⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ dom { ⟨ 𝑋 , 𝑌 ⟩ }
2		dmsnopss	⊢ dom { ⟨ 𝑋 , 𝑌 ⟩ } ⊆ { 𝑋 }
3	1 2	sstri	⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ { 𝑋 }