Theorem bj-vtoclg

Description: A version of vtoclg with an additional disjoint variable condition (which is removable if we allow use of df-clab , see bj-vtoclg1f ), which requires fewer axioms (i.e., removes dependency on ax-6 , ax-7 , ax-9 , ax-12 , ax-ext , df-clab , df-cleq , df-v ). (Contributed by BJ, 2-Jul-2022) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-vtoclg.maj	$$⊢x=A\to \left(\phi \to \psi \right)$$
	bj-vtoclg.min	$$⊢\phi$$
Assertion	bj-vtoclg	$$⊢A\in V\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclg.maj	$$⊢x=A\to \left(\phi \to \psi \right)$$
2		bj-vtoclg.min	$$⊢\phi$$
3		elissetv	$$⊢A\in V\to \exists xx=A$$
4	1 2	bj-exlimvmpi	$$⊢\exists xx=A\to \psi$$
5	3 4	syl	$$⊢A\in V\to \psi$$