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

Definition df-reu 2903
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wreu 2898 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1474 . . . . 5 class 𝑥
65, 3wcel 1977 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2458 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 195 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  3089  nfreud  3091  reubida  3101  reubiia  3104  reueq1f  3113  reu5  3136  rmo5  3139  cbvreu  3145  reuv  3194  reu2  3361  reu6  3362  reu3  3363  2reuswap  3377  2reu5lem1  3380  cbvreucsf  3533  reuss2  3866  reuun2  3869  reupick  3870  reupick3  3871  euelss  3873  reusn  4206  rabsneu  4208  reusv2lem4  4798  reusv2lem5  4799  reuhypd  4821  funcnv3  5873  feu  5993  dff4  6281  f1ompt  6290  fsn  6308  riotauni  6517  riotacl2  6524  riota1  6529  riota1a  6530  riota2df  6531  snriota  6540  riotaund  6546  aceq1  8823  dfac2  8836  nqerf  9631  zmin  11660  climreu  14135  divalglem10  14963  divalgb  14965  uptx  21238  txcn  21239  q1peqb  23718  axcontlem2  25645  frgra3vlem2  26528  3vfriswmgralem  26531  frgrancvvdeqlem3  26559  frgraeu  26581  adjeu  28132  2reuswap2  28712  rmoxfrdOLD  28716  rmoxfrd  28717  neibastop3  31527  poimirlem25  32604  poimirlem27  32606  edgnbusgreu  40595  nbusgredgeu0  40596  frgr3vlem2  41444  3vfriswmgrlem  41447  frgrncvvdeqlem3  41471  frgreu  41491
  Copyright terms: Public domain W3C validator