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	$$⊢\underset{\_}{Ⅎ}xA$$
	dvelimc.2	$$⊢\underset{\_}{Ⅎ}zB$$
	dvelimc.3	$$⊢z=y\to A=B$$
Assertion	dvelimc	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xB$$

Proof

Step	Hyp	Ref	Expression
1		dvelimc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dvelimc.2	$$⊢\underset{\_}{Ⅎ}zB$$
3		dvelimc.3	$$⊢z=y\to A=B$$
4		nftru	$$⊢Ⅎx\top$$
5		nftru	$$⊢Ⅎz\top$$
6	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
7	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}zB$$
8	3	a1i	$$⊢\top \to \left(z=y\to A=B\right)$$
9	4 5 6 7 8	dvelimdc	$$⊢\top \to \left(\neg \forall xx=y\to \underset{\_}{Ⅎ}xB\right)$$
10	9	mptru	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xB$$