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 xψ
bj-vtoclg1fv.maj x=Aφψ
bj-vtoclg1fv.min φ
Assertion bj-vtoclg1fv AVψ

Proof

Step Hyp Ref Expression
1 bj-vtoclg1fv.nf xψ
2 bj-vtoclg1fv.maj x=Aφψ
3 bj-vtoclg1fv.min φ
4 elissetv AVxx=A
5 1 2 3 bj-exlimmpi xx=Aψ
6 4 5 syl AVψ