mptssALT

Description: Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss . (Contributed by Thierry Arnoux, 30-May-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	mptssALT	$⊢ A \subseteq B \to (x \in A ⟼ C) \subseteq (x \in B ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	anim1d	$⊢ A \subseteq B \to ((x \in A \land y = C) \to (x \in B \land y = C))$
3	2	ssopab2dv	$⊢ A \subseteq B \to \{⟨x, y⟩ \| (x \in A \land y = C)\} \subseteq \{⟨x, y⟩ \| (x \in B \land y = C)\}$
4		df-mpt	$⊢ (x \in A ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
5		df-mpt	$⊢ (x \in B ⟼ C) = \{⟨x, y⟩ \| (x \in B \land y = C)\}$
6	3 4 5	3sstr4g	$⊢ A \subseteq B \to (x \in A ⟼ C) \subseteq (x \in B ⟼ C)$

Metamath Proof Explorer

Theorem mptssALT

Proof