Metamath Proof Explorer

Theorem prsssprel

Description: The elements of a pair from a subset of the set of all unordered pairs over a given set V are elements of the set V . (Contributed by AV, 21-Nov-2021)

		Ref	Expression
	Assertion	prsssprel	$⊢ (P \subseteq Pairs (V) \land \{X, Y\} \in P \land (X \in U \land Y \in W)) \to (X \in V \land Y \in V)$

Proof

Step	Hyp	Ref	Expression
1		ssel2	$⊢ (P \subseteq Pairs (V) \land \{X, Y\} \in P) \to \{X, Y\} \in Pairs (V)$
2		prsprel	$⊢ (\{X, Y\} \in Pairs (V) \land (X \in U \land Y \in W)) \to (X \in V \land Y \in V)$
3	1 2	stoic3	$⊢ (P \subseteq Pairs (V) \land \{X, Y\} \in P \land (X \in U \land Y \in W)) \to (X \in V \land Y \in V)$