Theorem iseqsetv-clel

Description: Alternate proof of iseqsetv-cleq . The expression E. x x = A does not depend on a particular choice of the set variable. Use this theorem in contexts where df-cleq or ax-ext is not referenced elsewhere in your proof. It is proven from a specific implementation (class builder, axiom df-clab ) of the primitive term x e. A . (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	iseqsetv-clel	$$⊢\exists xx=A\leftrightarrow \exists yy=A$$

Proof

Step	Hyp	Ref	Expression
1		issettru	$$⊢\exists xx=A\leftrightarrow A\in \left\{z|\top \right\}$$
2		issettru	$$⊢\exists yy=A\leftrightarrow A\in \left\{z|\top \right\}$$
3	1 2	bitr4i	$$⊢\exists xx=A\leftrightarrow \exists yy=A$$