prsprel

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

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

Proof

Step	Hyp	Ref	Expression
1		sprel	$⊢ \{X, Y\} \in Pairs (V) \to \exists a \in V \exists b \in V \{X, Y\} = \{a, b\}$
2		preq12bg	$⊢ ((X \in U \land Y \in W) \land (a \in V \land b \in V)) \to (\{X, Y\} = \{a, b\} \leftrightarrow ((X = a \land Y = b) \lor (X = b \land Y = a)))$
3		eleq1	$⊢ a = X \to (a \in V \leftrightarrow X \in V)$
4	3	eqcoms	$⊢ X = a \to (a \in V \leftrightarrow X \in V)$
5		eleq1	$⊢ b = Y \to (b \in V \leftrightarrow Y \in V)$
6	5	eqcoms	$⊢ Y = b \to (b \in V \leftrightarrow Y \in V)$
7	4 6	bi2anan9	$⊢ (X = a \land Y = b) \to ((a \in V \land b \in V) \leftrightarrow (X \in V \land Y \in V))$
8	7	biimpd	$⊢ (X = a \land Y = b) \to ((a \in V \land b \in V) \to (X \in V \land Y \in V))$
9		eleq1	$⊢ b = X \to (b \in V \leftrightarrow X \in V)$
10	9	eqcoms	$⊢ X = b \to (b \in V \leftrightarrow X \in V)$
11		eleq1	$⊢ a = Y \to (a \in V \leftrightarrow Y \in V)$
12	11	eqcoms	$⊢ Y = a \to (a \in V \leftrightarrow Y \in V)$
13	10 12	bi2anan9	$⊢ (X = b \land Y = a) \to ((b \in V \land a \in V) \leftrightarrow (X \in V \land Y \in V))$
14	13	biimpd	$⊢ (X = b \land Y = a) \to ((b \in V \land a \in V) \to (X \in V \land Y \in V))$
15	14	ancomsd	$⊢ (X = b \land Y = a) \to ((a \in V \land b \in V) \to (X \in V \land Y \in V))$
16	8 15	jaoi	$⊢ ((X = a \land Y = b) \lor (X = b \land Y = a)) \to ((a \in V \land b \in V) \to (X \in V \land Y \in V))$
17	16	com12	$⊢ (a \in V \land b \in V) \to (((X = a \land Y = b) \lor (X = b \land Y = a)) \to (X \in V \land Y \in V))$
18	17	adantl	$⊢ ((X \in U \land Y \in W) \land (a \in V \land b \in V)) \to (((X = a \land Y = b) \lor (X = b \land Y = a)) \to (X \in V \land Y \in V))$
19	2 18	sylbid	$⊢ ((X \in U \land Y \in W) \land (a \in V \land b \in V)) \to (\{X, Y\} = \{a, b\} \to (X \in V \land Y \in V))$
20	19	expcom	$⊢ (a \in V \land b \in V) \to ((X \in U \land Y \in W) \to (\{X, Y\} = \{a, b\} \to (X \in V \land Y \in V)))$
21	20	com23	$⊢ (a \in V \land b \in V) \to (\{X, Y\} = \{a, b\} \to ((X \in U \land Y \in W) \to (X \in V \land Y \in V)))$
22	21	rexlimivv	$⊢ \exists a \in V \exists b \in V \{X, Y\} = \{a, b\} \to ((X \in U \land Y \in W) \to (X \in V \land Y \in V))$
23	1 22	syl	$⊢ \{X, Y\} \in Pairs (V) \to ((X \in U \land Y \in W) \to (X \in V \land Y \in V))$
24	23	imp	$⊢ (\{X, Y\} \in Pairs (V) \land (X \in U \land Y \in W)) \to (X \in V \land Y \in V)$

Metamath Proof Explorer

Theorem prsprel

Proof