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

Definition df-reu 2424
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 2419 . 2  wff  E! x  e.  A  ph
52cv 1331 . . . . 5  class  x
65, 3wcel 1481 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2000 . 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  2605  nfreudxy  2607  reubida  2615  reubiia  2618  reueq1f  2627  reu5  2646  rmo5  2649  cbvreu  2655  reuv  2708  reu2  2875  reu6  2876  reu3  2877  2reuswapdc  2891  cbvreucsf  3068  reuss2  3360  reuun2  3363  reupick  3364  reupick3  3365  reusn  3601  rabsneu  3603  reuhypd  4399  funcnv3  5192  feu  5312  dff4im  5573  f1ompt  5578  fsn  5599  riotauni  5743  riotacl2  5750  riota1  5755  riota1a  5756  riota2df  5757  snriota  5766  riotaund  5771  acexmid  5780  climreu  11097  divalgb  11656  uptx  12480  txcn  12481  dedekindicc  12817  bdcriota  13250
  Copyright terms: Public domain W3C validator