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	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		bj-pr21val	⊢ pr1 ⦅ 𝐴 , 𝐵 ⦆ = 𝐴
2		bj-pr1ex	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V → pr1 ⦅ 𝐴 , 𝐵 ⦆ ∈ V )
3	1 2	eqeltrrid	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V → 𝐴 ∈ V )
4		bj-pr22val	⊢ pr2 ⦅ 𝐴 , 𝐵 ⦆ = 𝐵
5		bj-pr2ex	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V → pr2 ⦅ 𝐴 , 𝐵 ⦆ ∈ V )
6	4 5	eqeltrrid	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V → 𝐵 ∈ V )
7	3 6	jca	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8		df-bj-2upl	⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
9		bj-1uplex	⊢ ( ⦅ 𝐴 ⦆ ∈ V ↔ 𝐴 ∈ V )
10	9	biimpri	⊢ ( 𝐴 ∈ V → ⦅ 𝐴 ⦆ ∈ V )
11		snex	⊢ { 1o } ∈ V
12		bj-xtagex	⊢ ( { 1o } ∈ V → ( 𝐵 ∈ V → ( { 1o } × tag 𝐵 ) ∈ V ) )
13	11 12	ax-mp	⊢ ( 𝐵 ∈ V → ( { 1o } × tag 𝐵 ) ∈ V )
14		unexg	⊢ ( ( ⦅ 𝐴 ⦆ ∈ V ∧ ( { 1o } × tag 𝐵 ) ∈ V ) → ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) ∈ V )
15	10 13 14	syl2an	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) ) ∈ V )
16	8 15	eqeltrid	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⦅ 𝐴 , 𝐵 ⦆ ∈ V )
17	7 16	impbii	⊢ ( ⦅ 𝐴 , 𝐵 ⦆ ∈ V ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )