Theorem cdeqcv

Description: Conditional equality for set-to-class promotion. (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Assertion	cdeqcv	$$⊢CondEq\left(x=y\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x=y\to x=y$$
2	1	cdeqi	$$⊢CondEq\left(x=y\to x=y\right)$$