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 3088
Description: Define restricted existential uniqueness.

Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading 𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3086). (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 3083 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1507 . . . . 5 class 𝑥
65, 3wcel 2051 . . . 4 wff 𝑥𝐴
76, 1wa 387 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2584 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 198 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  reuanid  3262  nfreu1  3304  nfreud  3306  reubida  3319  reubidva  3320  reubiia  3323  reueq1f  3332  reueq1  3340  reu5  3363  rmo5  3367  reueubd  3369  cbvreu  3374  reuv  3435  reu2  3621  reu6  3622  reu3  3623  2reuswap  3642  2reuswap2  3643  2reu5lem1  3648  cbvreucsf  3815  reuss2  4164  reuun2  4167  reupick  4168  reupick3  4169  euelss  4171  reusn  4533  rabsneu  4535  reusv2lem4  5151  reusv2lem5  5152  reuhypd  5172  funcnv3  6254  feu  6380  dff4  6688  f1ompt  6696  fsn  6718  riotauni  6941  riotacl2  6948  riota1  6953  riota1a  6954  riota2df  6955  snriota  6965  riotaund  6971  aceq1  9335  dfac2b  9348  nqerf  10148  zmin  12156  climreu  14772  divalglem10  15611  divalgb  15613  uptx  21952  txcn  21953  q1peqb  24466  axcontlem2  26469  edgnbusgreu  26867  nbusgredgeu0  26868  frgr3vlem2  27823  3vfriswmgrlem  27826  frgrncvvdeqlem2  27849  adjeu  29462  rmoxfrd  30053  neibastop3  33268  cbvreud  34133  poimirlem25  34395  poimirlem27  34397  pairreueq  43072  prprsprreu  43081  prprreueq  43082
  Copyright terms: Public domain W3C validator