Metamath Proof Explorer


Theorem bj-vtocl

Description: Remove dependency on ax-ext , df-clab and df-cleq (and df-sb and df-v ) from vtocl . (Contributed by BJ, 6-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-vtocl.s A V
bj-vtocl.maj x = A φ ψ
bj-vtocl.min φ
Assertion bj-vtocl ψ

Proof

Step Hyp Ref Expression
1 bj-vtocl.s A V
2 bj-vtocl.maj x = A φ ψ
3 bj-vtocl.min φ
4 nfv x ψ
5 4 1 2 3 bj-vtoclf ψ