Theorem bj-issetwt

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

	Ref	Expression
Assertion	bj-issetwt	|- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. { x | ph } <-> E. z ( z = A /\ z e. { x | ph } ) )
2	1	a1i	|- ( A. x ph -> ( A e. { x | ph } <-> E. z ( z = A /\ z e. { x | ph } ) ) )
3		vexwt	|- ( A. x ph -> z e. { x | ph } )
4	3	biantrud	|- ( A. x ph -> ( z = A <-> ( z = A /\ z e. { x | ph } ) ) )
5	4	bicomd	|- ( A. x ph -> ( ( z = A /\ z e. { x | ph } ) <-> z = A ) )
6	5	exbidv	|- ( A. x ph -> ( E. z ( z = A /\ z e. { x | ph } ) <-> E. z z = A ) )
7		bj-denotes	|- ( E. z z = A <-> E. y y = A )
8	7	a1i	|- ( A. x ph -> ( E. z z = A <-> E. y y = A ) )
9	2 6 8	3bitrd	|- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) )