Theorem bj-elabd2ALT

Description: Alternate proof of elabd2 bypassing elab6g (and using sbiedvw instead of the A. x ( x = y -> ps ) idiom). (Contributed by BJ, 16-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bj-elabd2ALT.ex	$$⊢\phi \to A\in V$$
	bj-elabd2ALT.eq	$$⊢\phi \to B=\left\{x|\psi \right\}$$
	bj-elabd2ALT.is	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	bj-elabd2ALT	$$⊢\phi \to \left(A\in B\leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-elabd2ALT.ex	$$⊢\phi \to A\in V$$
2		bj-elabd2ALT.eq	$$⊢\phi \to B=\left\{x|\psi \right\}$$
3		bj-elabd2ALT.is	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		simpr	$$⊢\left(\phi \wedge y=A\right)\to y=A$$
5	2	eqcomd	$$⊢\phi \to \left\{x|\psi \right\}=B$$
6	5	adantr	$$⊢\left(\phi \wedge y=A\right)\to \left\{x|\psi \right\}=B$$
7	4 6	eleq12d	$$⊢\left(\phi \wedge y=A\right)\to \left(y\in \left\{x|\psi \right\}\leftrightarrow A\in B\right)$$
8		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
9	8	biimparc	$$⊢\left(y=A\wedge x=y\right)\to x=A$$
10	9	anim2i	$$⊢\left(\phi \wedge \left(y=A\wedge x=y\right)\right)\to \left(\phi \wedge x=A\right)$$
11	10	anassrs	$$⊢\left(\left(\phi \wedge y=A\right)\wedge x=y\right)\to \left(\phi \wedge x=A\right)$$
12	11 3	syl	$$⊢\left(\left(\phi \wedge y=A\right)\wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
13	12	sbiedvw	$$⊢\left(\phi \wedge y=A\right)\to \left(\left[y/x\right]\psi \leftrightarrow \chi \right)$$
14	7 13	bibi12d	$$⊢\left(\phi \wedge y=A\right)\to \left(\left(y\in \left\{x|\psi \right\}\leftrightarrow \left[y/x\right]\psi \right)\leftrightarrow \left(A\in B\leftrightarrow \chi \right)\right)$$
15		df-clab	$$⊢y\in \left\{x|\psi \right\}\leftrightarrow \left[y/x\right]\psi$$
16	15	a1i	$$⊢\phi \to \left(y\in \left\{x|\psi \right\}\leftrightarrow \left[y/x\right]\psi \right)$$
17	1 14 16	vtocld	$$⊢\phi \to \left(A\in B\leftrightarrow \chi \right)$$