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

Definition df-reu 2330
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 2325 . 2  wff  E! x  e.  A  ph
52cv 1258 . . . . 5  class  x
65, 3wcel 1409 . . . 4  wff  x  e.  A
76, 1wa 101 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 1916 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 102 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  2498  nfreudxy  2500  reubida  2508  reubiia  2511  reueq1f  2520  reu5  2539  rmo5  2542  cbvreu  2548  reuv  2590  reu2  2751  reu6  2752  reu3  2753  2reuswapdc  2765  cbvreucsf  2937  reuss2  3244  reuun2  3247  reupick  3248  reupick3  3249  reusn  3468  rabsneu  3470  reuhypd  4230  funcnv3  4988  feu  5099  dff4im  5340  f1ompt  5347  fsn  5362  riotauni  5501  riotacl2  5508  riota1  5513  riota1a  5514  riota2df  5515  snriota  5524  riotaund  5529  acexmid  5538  climreu  10048  bdcriota  10369
  Copyright terms: Public domain W3C validator