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

Definition df-reu 2400
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 2395 . 2  wff  E! x  e.  A  ph
52cv 1315 . . . . 5  class  x
65, 3wcel 1465 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 1977 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 104 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  2579  nfreudxy  2581  reubida  2589  reubiia  2592  reueq1f  2601  reu5  2620  rmo5  2623  cbvreu  2629  reuv  2679  reu2  2845  reu6  2846  reu3  2847  2reuswapdc  2861  cbvreucsf  3034  reuss2  3326  reuun2  3329  reupick  3330  reupick3  3331  reusn  3564  rabsneu  3566  reuhypd  4362  funcnv3  5155  feu  5275  dff4im  5534  f1ompt  5539  fsn  5560  riotauni  5704  riotacl2  5711  riota1  5716  riota1a  5717  riota2df  5718  snriota  5727  riotaund  5732  acexmid  5741  climreu  11021  divalgb  11534  uptx  12354  txcn  12355  dedekindicc  12691  bdcriota  12977
  Copyright terms: Public domain W3C validator