MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-reu Unicode version

Definition df-reu 2704
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  set  x
3 cA . . 3  class  A
41, 2, 3wreu 2699 . 2  wff  E! x  e.  A  ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2280 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 177 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  2870  nfreud  2872  reubida  2882  reubiia  2885  reueq1f  2894  reu5  2913  rmo5  2916  cbvreu  2922  reuv  2963  reu2  3114  reu6  3115  reu3  3116  2reuswap  3128  2reu5lem1  3131  cbvreucsf  3305  reuss2  3613  reuun2  3616  reupick  3617  reupick3  3618  reusn  3869  rabsneu  3871  reusv2lem4  4718  reusv2lem5  4719  reusv6OLD  4725  reusv7OLD  4726  reuhypd  4741  funcnv3  5503  feu  5610  dff4  5874  f1ompt  5882  fsn  5897  riotaeqdv  6541  riotauni  6547  riotacl2  6554  riota1  6559  riota1a  6560  riota2df  6561  snriota  6571  riotaprc  6578  aceq1  7987  dfac2  8000  nqerf  8796  zmin  10559  climreu  12338  divalglem10  12910  divalgb  12912  uptx  17645  txcn  17646  q1peqb  20065  adjeu  23380  2reuswap2  23963  rmoxfrdOLD  23967  rmoxfrd  23968  axcontlem2  25852  neibastop3  26328  frgra3vlem2  28249  3vfriswmgralem  28252  frgrancvvdeqlem3  28279  frgraeu  28301
  Copyright terms: Public domain W3C validator