Theorem bj-dvelimdv1

Description: Curried (exported) form of bj-dvelimdv (of course, one is directly provable from the other, but we keep this proof for illustration purposes). (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bj-dvelimdv.nf	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
2		bj-dvelimdv.is	⊢ ( 𝑧 = 𝑦 → ( 𝜒 ↔ 𝜓 ) )
3		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 )
4		bj-nfimt	⊢ ( Ⅎ 𝑥 𝑧 = 𝑦 → ( Ⅎ 𝑥 𝜒 → Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜒 ) ) )
5	3 1 4	syl2imc	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜒 ) ) )
6	5	alrimdv	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜒 ) ) )
7		bj-nfalt	⊢ ( ∀ 𝑧 Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜒 ) → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) )
8	2	equsalvw	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) ↔ 𝜓 )
9	8	nfbii	⊢ ( Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) ↔ Ⅎ 𝑥 𝜓 )
10	6 7 9	bj-syl66ib	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 ) )