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
|- F/ x ps
vtoclg1f.maj
|- ( x = A -> ( ph <-> ps ) )
vtoclg1f.min
|- ph
Assertion vtoclg1f
|- ( A e. V -> ps )

Proof

Step Hyp Ref Expression
1 vtoclg1f.nf
 |-  F/ x ps
2 vtoclg1f.maj
 |-  ( x = A -> ( ph <-> ps ) )
3 vtoclg1f.min
 |-  ph
4 elisset
 |-  ( A e. V -> E. x x = A )
5 3 2 mpbii
 |-  ( x = A -> ps )
6 1 5 exlimi
 |-  ( E. x x = A -> ps )
7 4 6 syl
 |-  ( A e. V -> ps )