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⦆\in \mathrm{V}\leftrightarrow A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		bj-pr11val	$$⊢pr1⦅A⦆=A$$
2		bj-pr1ex	$$⊢⦅A⦆\in \mathrm{V}\to pr1⦅A⦆\in \mathrm{V}$$
3	1 2	eqeltrrid	$$⊢⦅A⦆\in \mathrm{V}\to A\in \mathrm{V}$$
4		df-bj-1upl	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA$$
5		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
6		bj-xtagex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to \left(A\in \mathrm{V}\to \left\{\varnothing \right\}\times tagA\in \mathrm{V}\right)$$
7	5 6	ax-mp	$$⊢A\in \mathrm{V}\to \left\{\varnothing \right\}\times tagA\in \mathrm{V}$$
8	4 7	eqeltrid	$$⊢A\in \mathrm{V}\to ⦅A⦆\in \mathrm{V}$$
9	3 8	impbii	$$⊢⦅A⦆\in \mathrm{V}\leftrightarrow A\in \mathrm{V}$$