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 -> ( ph -> ps ) )
	bj-vtoclg.min	|- ph
Assertion	bj-vtoclg	|- ( A e. V -> ps )

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclg.maj	|- ( x = A -> ( ph -> ps ) )
2		bj-vtoclg.min	|- ph
3		elissetv	|- ( A e. V -> E. x x = A )
4	1 2	bj-exlimvmpi	|- ( E. x x = A -> ps )
5	3 4	syl	|- ( A e. V -> ps )