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

Proof

Step	Hyp	Ref	Expression
1		bj-vtocl.s	⊢ 𝐴 ∈ 𝑉
2		bj-vtocl.maj	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		bj-vtocl.min	⊢ 𝜑
4		nfv	⊢ Ⅎ 𝑥 𝜓
5	4 1 2 3	bj-vtoclf	⊢ 𝜓