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 |) e. _V <-> ( A e. _V /\ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		bj-pr21val	|- pr1 (| A ,, B |) = A
2		bj-pr1ex	|- ( (| A ,, B |) e. _V -> pr1 (| A ,, B |) e. _V )
3	1 2	eqeltrrid	|- ( (| A ,, B |) e. _V -> A e. _V )
4		bj-pr22val	|- pr2 (| A ,, B |) = B
5		bj-pr2ex	|- ( (| A ,, B |) e. _V -> pr2 (| A ,, B |) e. _V )
6	4 5	eqeltrrid	|- ( (| A ,, B |) e. _V -> B e. _V )
7	3 6	jca	|- ( (| A ,, B |) e. _V -> ( A e. _V /\ B e. _V ) )
8		df-bj-2upl	|- (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) )
9		bj-1uplex	|- ( (| A |) e. _V <-> A e. _V )
10	9	biimpri	|- ( A e. _V -> (| A |) e. _V )
11		snex	|- { 1o } e. _V
12		bj-xtagex	|- ( { 1o } e. _V -> ( B e. _V -> ( { 1o } X. tag B ) e. _V ) )
13	11 12	ax-mp	|- ( B e. _V -> ( { 1o } X. tag B ) e. _V )
14		unexg	|- ( ( (| A |) e. _V /\ ( { 1o } X. tag B ) e. _V ) -> ( (| A |) u. ( { 1o } X. tag B ) ) e. _V )
15	10 13 14	syl2an	|- ( ( A e. _V /\ B e. _V ) -> ( (| A |) u. ( { 1o } X. tag B ) ) e. _V )
16	8 15	eqeltrid	|- ( ( A e. _V /\ B e. _V ) -> (| A ,, B |) e. _V )
17	7 16	impbii	|- ( (| A ,, B |) e. _V <-> ( A e. _V /\ B e. _V ) )