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	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 ) )