Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfcdeq  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 x . 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 
Step  Hyp  Ref  Expression 

1  wph  . . 3  
2  vx  . . 3  
3  vy  . . 3  
4  1, 2, 3  wcdeq 3310  . 2 
5  2, 3  weq 1733  . . 3 
6  5, 1  wi 4  . 2 
7  4, 6  wb 184  1 
Colors of variables: wff setvar class 
This definition is referenced by: cdeqi 3312 cdeqri 3313 
Copyright terms: Public domain  W3C validator 