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

Definition df-reu 2362
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 2357 . 2  wff  E! x  e.  A  ph
52cv 1286 . . . . 5  class  x
65, 3wcel 1436 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 1945 . 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  2534  nfreudxy  2536  reubida  2544  reubiia  2547  reueq1f  2556  reu5  2575  rmo5  2578  cbvreu  2584  reuv  2632  reu2  2794  reu6  2795  reu3  2796  2reuswapdc  2808  cbvreucsf  2981  reuss2  3268  reuun2  3271  reupick  3272  reupick3  3273  reusn  3498  rabsneu  3500  reuhypd  4269  funcnv3  5043  feu  5158  dff4im  5410  f1ompt  5415  fsn  5434  riotauni  5577  riotacl2  5584  riota1  5589  riota1a  5590  riota2df  5591  snriota  5600  riotaund  5605  acexmid  5614  climreu  10583  divalgb  10831  bdcriota  11243
  Copyright terms: Public domain W3C validator