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\in V$$
	bj-vtocl.maj	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	bj-vtocl.min	$$⊢\phi$$
Assertion	bj-vtocl	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		bj-vtocl.s	$$⊢A\in V$$
2		bj-vtocl.maj	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		bj-vtocl.min	$$⊢\phi$$
4		nfv	$$⊢Ⅎx\psi$$
5	4 1 2 3	bj-vtoclf	$$⊢\psi$$