Theorem vtoclfOLD

Description: Obsolete version of vtoclf as of 26-Jan-2025. (Contributed by NM, 30-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vtoclf.1	|- F/ x ps
	vtoclf.2	|- A e. _V
	vtoclf.3	|- ( x = A -> ( ph <-> ps ) )
	vtoclf.4	|- ph
Assertion	vtoclfOLD	|- ps

Proof

Step	Hyp	Ref	Expression
1		vtoclf.1	|- F/ x ps
2		vtoclf.2	|- A e. _V
3		vtoclf.3	|- ( x = A -> ( ph <-> ps ) )
4		vtoclf.4	|- ph
5	2	isseti	|- E. x x = A
6	3	biimpd	|- ( x = A -> ( ph -> ps ) )
7	5 6	eximii	|- E. x ( ph -> ps )
8	1 7	19.36i	|- ( A. x ph -> ps )
9	8 4	mpg	|- ps