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

Metamath Proof Explorer

Theorem elpr2elpr

Description: For an element A of an unordered pair which is a subset of a given set V , there is another (maybe the same) element b of the given set V being an element of the unordered pair. (Contributed by AV, 5-Dec-2020)

		Ref	Expression
	Assertion	elpr2elpr	$⊢ (X \in V \land Y \in V \land A \in \{X, Y\}) \to \exists b \in V \{X, Y\} = \{A, b\}$

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ (A = X \land (X \in V \land Y \in V)) \to Y \in V$
2		preq12	$⊢ (A = X \land b = Y) \to \{A, b\} = \{X, Y\}$
3	2	eqcomd	$⊢ (A = X \land b = Y) \to \{X, Y\} = \{A, b\}$
4	3	adantlr	$⊢ ((A = X \land (X \in V \land Y \in V)) \land b = Y) \to \{X, Y\} = \{A, b\}$
5	1 4	rspcedeq2vd	$⊢ (A = X \land (X \in V \land Y \in V)) \to \exists b \in V \{X, Y\} = \{A, b\}$
6	5	ex	$⊢ A = X \to ((X \in V \land Y \in V) \to \exists b \in V \{X, Y\} = \{A, b\})$
7		simprl	$⊢ (A = Y \land (X \in V \land Y \in V)) \to X \in V$
8		preq12	$⊢ (A = Y \land b = X) \to \{A, b\} = \{Y, X\}$
9		prcom	$⊢ \{Y, X\} = \{X, Y\}$
10	8 9	eqtr2di	$⊢ (A = Y \land b = X) \to \{X, Y\} = \{A, b\}$
11	10	adantlr	$⊢ ((A = Y \land (X \in V \land Y \in V)) \land b = X) \to \{X, Y\} = \{A, b\}$
12	7 11	rspcedeq2vd	$⊢ (A = Y \land (X \in V \land Y \in V)) \to \exists b \in V \{X, Y\} = \{A, b\}$
13	12	ex	$⊢ A = Y \to ((X \in V \land Y \in V) \to \exists b \in V \{X, Y\} = \{A, b\})$
14	6 13	jaoi	$⊢ (A = X \lor A = Y) \to ((X \in V \land Y \in V) \to \exists b \in V \{X, Y\} = \{A, b\})$
15		elpri	$⊢ A \in \{X, Y\} \to (A = X \lor A = Y)$
16	14 15	syl11	$⊢ (X \in V \land Y \in V) \to (A \in \{X, Y\} \to \exists b \in V \{X, Y\} = \{A, b\})$
17	16	3impia	$⊢ (X \in V \land Y \in V \land A \in \{X, Y\}) \to \exists b \in V \{X, Y\} = \{A, b\}$