Theorem bj-vtoclf

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

	Ref	Expression
Hypotheses	bj-vtoclf.nf	⊢ Ⅎ 𝑥 𝜓
	bj-vtoclf.s	⊢ 𝐴 ∈ 𝑉
	bj-vtoclf.maj	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	bj-vtoclf.min	⊢ 𝜑
Assertion	bj-vtoclf	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclf.nf	⊢ Ⅎ 𝑥 𝜓
2		bj-vtoclf.s	⊢ 𝐴 ∈ 𝑉
3		bj-vtoclf.maj	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		bj-vtoclf.min	⊢ 𝜑
5	2	bj-issetiv	⊢ ∃ 𝑥 𝑥 = 𝐴
6	3	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝜑 → 𝜓 ) )
7	5 6	eximii	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
8	1 7	19.36i	⊢ ( ∀ 𝑥 𝜑 → 𝜓 )
9	8 4	mpg	⊢ 𝜓