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	|- F/_ x A
	dvelimc.2	|- F/_ z B
	dvelimc.3	|- ( z = y -> A = B )
Assertion	dvelimc	|- ( -. A. x x = y -> F/_ x B )

Proof

Step	Hyp	Ref	Expression
1		dvelimc.1	|- F/_ x A
2		dvelimc.2	|- F/_ z B
3		dvelimc.3	|- ( z = y -> A = B )
4		nftru	|- F/ x T.
5		nftru	|- F/ z T.
6	1	a1i	|- ( T. -> F/_ x A )
7	2	a1i	|- ( T. -> F/_ z B )
8	3	a1i	|- ( T. -> ( z = y -> A = B ) )
9	4 5 6 7 8	dvelimdc	|- ( T. -> ( -. A. x x = y -> F/_ x B ) )
10	9	mptru	|- ( -. A. x x = y -> F/_ x B )