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

Definition df-reu 2553
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 2548 . 2  wff  E! x  e.  A  ph
52cv 1624 . . . . 5  class  x
65, 3wcel 1687 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2weu 2146 . 2  wff  E! x
( x  e.  A  /\  ph )
94, 8wb 178 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  2713  nfreud  2715  reubida  2725  reubiia  2728  reueq1f  2737  reu5  2756  rmo5  2759  cbvreu  2765  reuv  2806  reu2  2956  reu6  2957  reu3  2958  2reuswap  2970  2reu5lem1  2973  cbvreucsf  3148  reuss2  3451  reuun2  3454  reupick  3455  reupick3  3456  reusn  3703  rabsneu  3705  reusv2lem4  4539  reusv2lem5  4540  reusv6OLD  4546  reusv7OLD  4547  reuhypd  4562  funcnv3  5278  feu  5384  dff4  5637  f1ompt  5645  fsn  5659  riotaeqdv  6302  riotauni  6308  riotacl2  6315  riota1  6320  riota1a  6321  riota2df  6322  snriota  6332  riotaprc  6339  aceq1  7741  dfac2  7754  nqerf  8551  zmin  10309  climreu  12026  divalglem10  12597  divalgb  12599  uptx  17315  txcn  17316  q1peqb  19536  adjeu  22463  axcontlem2  24002  neibastop3  25712
  Copyright terms: Public domain W3C validator