This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvelimdc

Description: Deduction form of dvelimc . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimdc.1 ⊢ Ⅎ 𝑥 𝜑
dvelimdc.2 ⊢ Ⅎ 𝑧 𝜑
dvelimdc.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
dvelimdc.4 ⊢ ( 𝜑 → Ⅎ 𝑧 𝐵 )
dvelimdc.5 ⊢ ( 𝜑 → ( 𝑧 = 𝑦 → 𝐴 = 𝐵 ) )
Assertion dvelimdc ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvelimdc.1 ⊢ Ⅎ 𝑥 𝜑
2 dvelimdc.2 ⊢ Ⅎ 𝑧 𝜑
3 dvelimdc.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
4 dvelimdc.4 ⊢ ( 𝜑 → Ⅎ 𝑧 𝐵 )
5 dvelimdc.5 ⊢ ( 𝜑 → ( 𝑧 = 𝑦 → 𝐴 = 𝐵 ) )
6 nfv ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
7 3 nfcrd ⊢ ( 𝜑 → Ⅎ 𝑥 𝑤 ∈ 𝐴 )
8 4 nfcrd ⊢ ( 𝜑 → Ⅎ 𝑧 𝑤 ∈ 𝐵 )
9 eleq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ 𝐵 ) )
10 5 9 syl6 ⊢ ( 𝜑 → ( 𝑧 = 𝑦 → ( 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ 𝐵 ) ) )
11 1 2 7 8 10 dvelimdf ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 ∈ 𝐵 ) )
12 11 imp ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑤 ∈ 𝐵 )
13 6 12 nfcd ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝐵 )
14 13 ex ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 ) )