Metamath Proof Explorer


Theorem bj-vtoclg1fv

Description: Version of bj-vtoclg1f with a disjoint variable condition on x , V . This removes dependency on df-sb and df-clab . Prefer its use over bj-vtoclg1f when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 14-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-vtoclg1fv.nf
|- F/ x ps
bj-vtoclg1fv.maj
|- ( x = A -> ( ph -> ps ) )
bj-vtoclg1fv.min
|- ph
Assertion bj-vtoclg1fv
|- ( A e. V -> ps )

Proof

Step Hyp Ref Expression
1 bj-vtoclg1fv.nf
 |-  F/ x ps
2 bj-vtoclg1fv.maj
 |-  ( x = A -> ( ph -> ps ) )
3 bj-vtoclg1fv.min
 |-  ph
4 elissetv
 |-  ( A e. V -> E. x x = A )
5 1 2 3 bj-exlimmpi
 |-  ( E. x x = A -> ps )
6 4 5 syl
 |-  ( A e. V -> ps )