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

Definition df-reu 2360
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu  |-  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3wreu 2355 . 2  wff  E! x  e.  A  ph
52cv 1284 . . . . 5  class  x
65, 3wcel 1434 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 1943 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 103 1  wff  ( E! x  e.  A  ph  <->  E! x ( x  e.  A  /\  ph )
)
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2531  nfreudxy  2533  reubida  2541  reubiia  2544  reueq1f  2553  reu5  2572  rmo5  2575  cbvreu  2581  reuv  2629  reu2  2791  reu6  2792  reu3  2793  2reuswapdc  2805  cbvreucsf  2977  reuss2  3262  reuun2  3265  reupick  3266  reupick3  3267  reusn  3487  rabsneu  3489  reuhypd  4257  funcnv3  5029  feu  5141  dff4im  5390  f1ompt  5395  fsn  5411  riotauni  5553  riotacl2  5560  riota1  5565  riota1a  5566  riota2df  5567  snriota  5576  riotaund  5581  acexmid  5590  climreu  10510  divalgb  10705  bdcriota  11117
  Copyright terms: Public domain W3C validator