Metamath Proof Explorer


Theorem cdeqcv

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

Ref Expression
Assertion cdeqcv CondEqx=yx=y

Proof

Step Hyp Ref Expression
1 id x=yx=y
2 1 cdeqi CondEqx=yx=y