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 |) e. _V <-> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		bj-pr11val	|- pr1 (| A |) = A
2		bj-pr1ex	|- ( (| A |) e. _V -> pr1 (| A |) e. _V )
3	1 2	eqeltrrid	|- ( (| A |) e. _V -> A e. _V )
4		df-bj-1upl	|- (| A |) = ( { (/) } X. tag A )
5		p0ex	|- { (/) } e. _V
6		bj-xtagex	|- ( { (/) } e. _V -> ( A e. _V -> ( { (/) } X. tag A ) e. _V ) )
7	5 6	ax-mp	|- ( A e. _V -> ( { (/) } X. tag A ) e. _V )
8	4 7	eqeltrid	|- ( A e. _V -> (| A |) e. _V )
9	3 8	impbii	|- ( (| A |) e. _V <-> A e. _V )