Theorem bj-issetwt

Description: Closed form of bj-issetw . (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-issetwt	$$⊢\forall x\phi \to \left(A\in \left\{x|\phi \right\}\leftrightarrow \exists yy=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \exists z\left(z=A\wedge z\in \left\{x|\phi \right\}\right)$$
2	1	a1i	$$⊢\forall x\phi \to \left(A\in \left\{x|\phi \right\}\leftrightarrow \exists z\left(z=A\wedge z\in \left\{x|\phi \right\}\right)\right)$$
3		vexwt	$$⊢\forall x\phi \to z\in \left\{x|\phi \right\}$$
4	3	biantrud	$$⊢\forall x\phi \to \left(z=A\leftrightarrow \left(z=A\wedge z\in \left\{x|\phi \right\}\right)\right)$$
5	4	bicomd	$$⊢\forall x\phi \to \left(\left(z=A\wedge z\in \left\{x|\phi \right\}\right)\leftrightarrow z=A\right)$$
6	5	exbidv	$$⊢\forall x\phi \to \left(\exists z\left(z=A\wedge z\in \left\{x|\phi \right\}\right)\leftrightarrow \exists zz=A\right)$$
7		iseqsetv-clel	$$⊢\exists zz=A\leftrightarrow \exists yy=A$$
8	7	a1i	$$⊢\forall x\phi \to \left(\exists zz=A\leftrightarrow \exists yy=A\right)$$
9	2 6 8	3bitrd	$$⊢\forall x\phi \to \left(A\in \left\{x|\phi \right\}\leftrightarrow \exists yy=A\right)$$