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