Metamath Proof Explorer

Theorem bj-1uplex

Description: A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-1uplex ⊢ A ∈ V ↔ A ∈ V

Proof

Step Hyp Ref Expression
1 bj-pr11val ⊢ pr1 A = A
2 bj-pr1ex ⊢ A ∈ V → pr1 A ∈ V
3 1 2 eqeltrrid ⊢ A ∈ V → A ∈ V
4 df-bj-1upl ⊢ A = ∅ × tag A
5 p0ex ⊢ ∅ ∈ V
6 bj-xtagex ⊢ ∅ ∈ V → A ∈ V → ∅ × tag A ∈ V
7 5 6 ax-mp ⊢ A ∈ V → ∅ × tag A ∈ V
8 4 7 eqeltrid ⊢ A ∈ V → A ∈ V
9 3 8 impbii ⊢ A ∈ V ↔ A ∈ V