Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfcdeq  Structured version Unicode version 
Description: Define conditional equality. All the notation to the left of the is fake; the parentheses and arrows are all part of the notation, which could equally well be written CondEq. On the right side is the actual implication arrow. The reason for this definition is to "flatten" the structure on the right side (whose tree structure is something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy wph). (Contributed by Mario Carneiro, 11Aug2016.) 
Ref  Expression 

dfcdeq  CondEq 
Step  Hyp  Ref  Expression 

1  wph  . . 3  
2  vx  . . 3  
3  vy  . . 3  
4  1, 2, 3  wcdeq 3144  . 2 CondEq 
5  2, 3  weq 1653  . . 3 
6  5, 1  wi 4  . 2 
7  4, 6  wb 177  1 CondEq 
Colors of variables: wff set class 
This definition is referenced by: cdeqi 3146 cdeqri 3147 
Copyright terms: Public domain  W3C validator 