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

Proof

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