ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-cdeq Unicode version

Definition df-cdeq 2893
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 y ph. 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, 11-Aug-2016.)
Assertion
Ref Expression
df-cdeq  |-  (CondEq (
x  =  y  ->  ph )  <->  ( x  =  y  ->  ph ) )

Detailed syntax breakdown of Definition df-cdeq
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
41, 2, 3wcdeq 2892 . 2  wff CondEq ( x  =  y  ->  ph )
52, 3weq 1479 . . 3  wff  x  =  y
65, 1wi 4 . 2  wff  ( x  =  y  ->  ph )
74, 6wb 104 1  wff  (CondEq (
x  =  y  ->  ph )  <->  ( x  =  y  ->  ph ) )
Colors of variables: wff set class
This definition is referenced by:  cdeqi  2894  cdeqri  2895  bdcdeq  13142
  Copyright terms: Public domain W3C validator