Metamath Proof Explorer

Theorem cdeqcv

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

Ref Expression
Assertion cdeqcv 
|- CondEq ( x = y -> x = y )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = y -> x = y )
2 1 cdeqi 
 |-  CondEq ( x = y -> x = y )