Description: Deduction form of dvelimf . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvelimdf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
dvelimdf.2 | ⊢ Ⅎ 𝑧 𝜑 | ||
dvelimdf.3 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | ||
dvelimdf.4 | ⊢ ( 𝜑 → Ⅎ 𝑧 𝜒 ) | ||
dvelimdf.5 | ⊢ ( 𝜑 → ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) ) | ||
Assertion | dvelimdf | ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvelimdf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
2 | dvelimdf.2 | ⊢ Ⅎ 𝑧 𝜑 | |
3 | dvelimdf.3 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | |
4 | dvelimdf.4 | ⊢ ( 𝜑 → Ⅎ 𝑧 𝜒 ) | |
5 | dvelimdf.5 | ⊢ ( 𝜑 → ( 𝑧 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) ) | |
6 | 1 3 | nfim1 | ⊢ Ⅎ 𝑥 ( 𝜑 → 𝜓 ) |
7 | 2 4 | nfim1 | ⊢ Ⅎ 𝑧 ( 𝜑 → 𝜒 ) |
8 | 5 | com12 | ⊢ ( 𝑧 = 𝑦 → ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) ) |
9 | 8 | pm5.74d | ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) ) |
10 | 6 7 9 | dvelimf | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( 𝜑 → 𝜒 ) ) |
11 | pm5.5 | ⊢ ( 𝜑 → ( ( 𝜑 → 𝜒 ) ↔ 𝜒 ) ) | |
12 | 1 11 | nfbidf | ⊢ ( 𝜑 → ( Ⅎ 𝑥 ( 𝜑 → 𝜒 ) ↔ Ⅎ 𝑥 𝜒 ) ) |
13 | 10 12 | syl5ib | ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜒 ) ) |