Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvelimf-o.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	dvelimf-o.2	⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
	dvelimf-o.3	⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	dvelimf-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		dvelimf-o.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		dvelimf-o.2	⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
3		dvelimf-o.3	⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		hba1-o	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) )
5		ax-c11	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
6	5	aecoms-o	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
7	4 6	syl5	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
8	7	a1d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) ) )
9		hbnae-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑧 )
10		hbnae-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )
11	9 10	hban	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ∀ 𝑧 ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
12		hbnae-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧 )
13		hbnae-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )
14	12 13	hban	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ∀ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
15		ax-c9	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) )
16	15	imp	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
17	1	a1i	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 𝜑 ) )
18	14 16 17	hbimd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑧 = 𝑦 → 𝜑 ) ) )
19	11 18	hbald	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
20	19	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) ) )
21	8 20	pm2.61i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) )
22	2 3	equsalh	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ 𝜓 )
23	22	albii	⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 𝜓 )
24	21 22 23	3imtr3g	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )