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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
	bj-vtoclg.min	⊢ 𝜑
Assertion	bj-vtoclg	⊢ ( 𝐴 ∈ 𝑉 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclg.maj	⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
2		bj-vtoclg.min	⊢ 𝜑
3		elissetv	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
4	1 2	bj-exlimvmpi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 )
5	3 4	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝜓 )