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 𝑥 𝜓
bj-vtoclg1fv.maj ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
bj-vtoclg1fv.min 𝜑
Assertion bj-vtoclg1fv ( 𝐴𝑉𝜓 )

Proof

Step Hyp Ref Expression
1 bj-vtoclg1fv.nf 𝑥 𝜓
2 bj-vtoclg1fv.maj ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
3 bj-vtoclg1fv.min 𝜑
4 elissetv ( 𝐴𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
5 1 2 3 bj-exlimmpi ( ∃ 𝑥 𝑥 = 𝐴𝜓 )
6 4 5 syl ( 𝐴𝑉𝜓 )