Metamath Proof Explorer

Theorem bj-2uplex

Description: A couple is a set if and only if its coordinates are sets. For the advantages offered by the reverse closure property, see the section head comment. (Contributed by BJ, 6-Oct-2018)

		Ref	Expression
	Assertion	bj-2uplex	$⊢ ⦅A, B⦆ \in V \leftrightarrow (A \in V \land B \in V)$

Proof

Step	Hyp	Ref	Expression
1		bj-pr21val	$⊢ pr1 ⦅A, B⦆ = A$
2		bj-pr1ex	$⊢ ⦅A, B⦆ \in V \to pr1 ⦅A, B⦆ \in V$
3	1 2	eqeltrrid	$⊢ ⦅A, B⦆ \in V \to A \in V$
4		bj-pr22val	$⊢ pr2 ⦅A, B⦆ = B$
5		bj-pr2ex	$⊢ ⦅A, B⦆ \in V \to pr2 ⦅A, B⦆ \in V$
6	4 5	eqeltrrid	$⊢ ⦅A, B⦆ \in V \to B \in V$
7	3 6	jca	$⊢ ⦅A, B⦆ \in V \to (A \in V \land B \in V)$
8		df-bj-2upl	$⊢ ⦅A, B⦆ = ⦅A⦆ \cup (\{1_{𝑜}\} \times tag B)$
9		bj-1uplex	$⊢ ⦅A⦆ \in V \leftrightarrow A \in V$
10	9	biimpri	$⊢ A \in V \to ⦅A⦆ \in V$
11		snex	$⊢ \{1_{𝑜}\} \in V$
12		bj-xtagex	$⊢ \{1_{𝑜}\} \in V \to (B \in V \to \{1_{𝑜}\} \times tag B \in V)$
13	11 12	ax-mp	$⊢ B \in V \to \{1_{𝑜}\} \times tag B \in V$
14		unexg	$⊢ (⦅A⦆ \in V \land \{1_{𝑜}\} \times tag B \in V) \to ⦅A⦆ \cup (\{1_{𝑜}\} \times tag B) \in V$
15	10 13 14	syl2an	$⊢ (A \in V \land B \in V) \to ⦅A⦆ \cup (\{1_{𝑜}\} \times tag B) \in V$
16	8 15	eqeltrid	$⊢ (A \in V \land B \in V) \to ⦅A, B⦆ \in V$
17	7 16	impbii	$⊢ ⦅A, B⦆ \in V \leftrightarrow (A \in V \land B \in V)$