Theorem bj-vtocl

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-vtocl.s	|- A e. V
2		bj-vtocl.maj	|- ( x = A -> ( ph <-> ps ) )
3		bj-vtocl.min	|- ph
4		nfv	|- F/ x ps
5	4 1 2 3	bj-vtoclf	|- ps