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

Metamath Proof Explorer

Theorem dvelimc

Description: Version of dvelim for classes. 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	dvelimc.1	⊢ Ⅎ 𝑥 𝐴
	dvelimc.2	⊢ Ⅎ 𝑧 𝐵
	dvelimc.3	⊢ ( 𝑧 = 𝑦 → 𝐴 = 𝐵 )
Assertion	dvelimc	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dvelimc.1	⊢ Ⅎ 𝑥 𝐴
2		dvelimc.2	⊢ Ⅎ 𝑧 𝐵
3		dvelimc.3	⊢ ( 𝑧 = 𝑦 → 𝐴 = 𝐵 )
4		nftru	⊢ Ⅎ 𝑥 ⊤
5		nftru	⊢ Ⅎ 𝑧 ⊤
6	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 )
7	2	a1i	⊢ ( ⊤ → Ⅎ 𝑧 𝐵 )
8	3	a1i	⊢ ( ⊤ → ( 𝑧 = 𝑦 → 𝐴 = 𝐵 ) )
9	4 5 6 7 8	dvelimdc	⊢ ( ⊤ → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 ) )
10	9	mptru	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝐵 )