Theorem bj-vtoclf

Description: Remove dependency on ax-ext , df-clab and df-cleq (and df-sb and df-v ) from vtoclf . (Contributed by BJ, 6-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-vtoclf.nf	|- F/ x ps
	bj-vtoclf.s	|- A e. V
	bj-vtoclf.maj	|- ( x = A -> ( ph <-> ps ) )
	bj-vtoclf.min	|- ph
Assertion	bj-vtoclf	|- ps

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclf.nf	|- F/ x ps
2		bj-vtoclf.s	|- A e. V
3		bj-vtoclf.maj	|- ( x = A -> ( ph <-> ps ) )
4		bj-vtoclf.min	|- ph
5	2	bj-issetiv	|- 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