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

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclf.nf	$$⊢Ⅎx\psi$$
2		bj-vtoclf.s	$$⊢A\in V$$
3		bj-vtoclf.maj	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		bj-vtoclf.min	$$⊢\phi$$
5	2	bj-issetiv	$$⊢\exists xx=A$$
6	3	biimpd	$$⊢x=A\to \left(\phi \to \psi \right)$$
7	5 6	eximii	$$⊢\exists x\left(\phi \to \psi \right)$$
8	1 7	19.36i	$$⊢\forall x\phi \to \psi$$
9	8 4	mpg	$$⊢\psi$$