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 V A V B V

Proof

Step Hyp Ref Expression
1 bj-pr21val pr1 A B = A
2 bj-pr1ex A B V pr1 A B V
3 1 2 eqeltrrid A B V A V
4 bj-pr22val pr2 A B = B
5 bj-pr2ex A B V pr2 A B V
6 4 5 eqeltrrid A B V B V
7 3 6 jca A B V A V B V
8 df-bj-2upl A B = A 1 𝑜 × tag B
9 bj-1uplex A V A V
10 9 biimpri A V A V
11 snex 1 𝑜 V
12 bj-xtagex 1 𝑜 V B V 1 𝑜 × tag B V
13 11 12 ax-mp B V 1 𝑜 × tag B V
14 unexg A V 1 𝑜 × tag B V A 1 𝑜 × tag B V
15 10 13 14 syl2an A V B V A 1 𝑜 × tag B V
16 8 15 eqeltrid A V B V A B V
17 7 16 impbii A B V A V B V