Theorem bj-clel3gALT

Description: Alternate proof of clel3g . (Contributed by BJ, 1-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-clel3gALT	$$⊢B\in V\to \left(A\in B\leftrightarrow \exists x\left(x=B\wedge A\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elisset	$$⊢B\in V\to \exists xx=B$$
2	1	biantrurd	$$⊢B\in V\to \left(A\in B\leftrightarrow \left(\exists xx=B\wedge A\in B\right)\right)$$
3		19.41v	$$⊢\exists x\left(x=B\wedge A\in B\right)\leftrightarrow \left(\exists xx=B\wedge A\in B\right)$$
4	2 3	bitr4di	$$⊢B\in V\to \left(A\in B\leftrightarrow \exists x\left(x=B\wedge A\in B\right)\right)$$
5		eleq2	$$⊢x=B\to \left(A\in x\leftrightarrow A\in B\right)$$
6	5	bicomd	$$⊢x=B\to \left(A\in B\leftrightarrow A\in x\right)$$
7	6	pm5.32i	$$⊢\left(x=B\wedge A\in B\right)\leftrightarrow \left(x=B\wedge A\in x\right)$$
8	7	exbii	$$⊢\exists x\left(x=B\wedge A\in B\right)\leftrightarrow \exists x\left(x=B\wedge A\in x\right)$$
9	4 8	bitrdi	$$⊢B\in V\to \left(A\in B\leftrightarrow \exists x\left(x=B\wedge A\in x\right)\right)$$