Theorem bj-dvelimv

Description: A version of dvelim using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-dvelimv.nf	⊢ Ⅎ 𝑥 𝜓
	bj-dvelimv.is	⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
Assertion	bj-dvelimv	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-dvelimv.nf	⊢ Ⅎ 𝑥 𝜓
2		bj-dvelimv.is	⊢ ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
3	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜓 )
4	3 2	bj-dvelimdv1	⊢ ( ⊤ → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 ) )
5	4	mptru	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )