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

Definition df-reu 2673
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 2668 . 2  wff  E! x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2254 . 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  2838  nfreud  2840  reubida  2850  reubiia  2853  reueq1f  2862  reu5  2881  rmo5  2884  cbvreu  2890  reuv  2931  reu2  3082  reu6  3083  reu3  3084  2reuswap  3096  2reu5lem1  3099  cbvreucsf  3273  reuss2  3581  reuun2  3584  reupick  3585  reupick3  3586  reusn  3837  rabsneu  3839  reusv2lem4  4686  reusv2lem5  4687  reusv6OLD  4693  reusv7OLD  4694  reuhypd  4709  funcnv3  5471  feu  5578  dff4  5842  f1ompt  5850  fsn  5865  riotaeqdv  6509  riotauni  6515  riotacl2  6522  riota1  6527  riota1a  6528  riota2df  6529  snriota  6539  riotaprc  6546  aceq1  7954  dfac2  7967  nqerf  8763  zmin  10526  climreu  12305  divalglem10  12877  divalgb  12879  uptx  17610  txcn  17611  q1peqb  20030  adjeu  23345  2reuswap2  23928  rmoxfrdOLD  23932  rmoxfrd  23933  axcontlem2  25808  neibastop3  26281  frgra3vlem2  28105  3vfriswmgralem  28108  frgrancvvdeqlem3  28135  frgraeu  28157
  Copyright terms: Public domain W3C validator