Metamath Proof Explorer

Theorem vtoclg1f

Description: Version of vtoclgf with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 and ax-13 . (Contributed by BJ, 1-May-2019)

Ref Expression
Hypotheses x ψ
vtoclg1f.maj x = A φ ψ
vtoclg1f.min φ
Assertion vtoclg1f A V ψ


Step Hyp Ref Expression
1 x ψ
2 vtoclg1f.maj x = A φ ψ
3 vtoclg1f.min φ
4 elisset A V x x = A
5 3 2 mpbii x = A ψ
6 1 5 exlimi x x = A ψ
7 4 6 syl A V ψ