Theorem bj-vtoclgfALT

Description: Alternate proof of vtoclgf . Proof from vtoclgft . (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bj-vtoclgfALT.1	$$⊢\underset{\_}{Ⅎ}xA$$
	bj-vtoclgfALT.2	$$⊢Ⅎx\psi$$
	bj-vtoclgfALT.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	bj-vtoclgfALT.4	$$⊢\phi$$
Assertion	bj-vtoclgfALT	$$⊢A\in V\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclgfALT.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		bj-vtoclgfALT.2	$$⊢Ⅎx\psi$$
3		bj-vtoclgfALT.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		bj-vtoclgfALT.4	$$⊢\phi$$
5	1 2	pm3.2i	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)$$
6	3	ax-gen	$$⊢\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)$$
7	4	ax-gen	$$⊢\forall x\phi$$
8	6 7	pm3.2i	$$⊢\left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)$$
9		vtoclgft	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\wedge A\in V\right)\to \psi$$
10	5 8 9	mp3an12	$$⊢A\in V\to \psi$$