Metamath Proof Explorer


Theorem vtoclg1f

Description: Version of vtoclgf with one nonfreeness 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 vtoclg1f.nf x ψ
vtoclg1f.maj x = A φ ψ
vtoclg1f.min φ
Assertion vtoclg1f A V ψ

Proof

Step Hyp Ref Expression
1 vtoclg1f.nf 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 ψ