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	|- F/_ x A
	bj-vtoclgfALT.2	|- F/ x ps
	bj-vtoclgfALT.3	|- ( x = A -> ( ph <-> ps ) )
	bj-vtoclgfALT.4	|- ph
Assertion	bj-vtoclgfALT	|- ( A e. V -> ps )

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclgfALT.1	|- F/_ x A
2		bj-vtoclgfALT.2	|- F/ x ps
3		bj-vtoclgfALT.3	|- ( x = A -> ( ph <-> ps ) )
4		bj-vtoclgfALT.4	|- ph
5	1 2	pm3.2i	|- ( F/_ x A /\ F/ x ps )
6	3	ax-gen	|- A. x ( x = A -> ( ph <-> ps ) )
7	4	ax-gen	|- A. x ph
8	6 7	pm3.2i	|- ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph )
9		vtoclgft	|- ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )
10	5 8 9	mp3an12	|- ( A e. V -> ps )