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 3140
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 3138). (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 3135 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2115 . . . 4 wff 𝑥𝐴
76, 1wa 399 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2654 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 209 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  reuanid  3319  nfreu1  3361  nfreud  3363  nfreuw  3365  reubida  3378  reubidva  3379  reubiia  3381  reueq1f  3390  reueq1  3398  reu5  3413  rmo5  3417  reueubd  3419  cbvreuw  3427  cbvreu  3432  reuv  3507  reu2  3702  reu6  3703  reu3  3704  2reuswap  3723  2reuswap2  3724  2reu5lem1  3732  cbvreucsf  3910  reuss2  4268  reuun2  4271  reupick  4272  reupick3  4273  euelss  4275  reusn  4648  rabsneu  4650  reusv2lem4  5290  reusv2lem5  5291  reuhypd  5308  funcnv3  6414  feu  6546  dff4  6860  f1ompt  6868  fsn  6890  riotauni  7115  riotacl2  7125  riota1  7130  riota1a  7131  riota2df  7132  snriota  7142  riotaund  7148  aceq1  9543  dfac2b  9556  nqerf  10352  zmin  12343  climreu  14915  divalglem10  15753  divalgb  15755  uptx  22239  txcn  22240  q1peqb  24764  axcontlem2  26768  edgnbusgreu  27166  nbusgredgeu0  27167  frgr3vlem2  28068  3vfriswmgrlem  28071  frgrncvvdeqlem2  28094  adjeu  29681  reuxfrdf  30271  rmoxfrd  30273  neibastop3  33795  cbvreud  34762  poimirlem25  35054  poimirlem27  35056  fsuppind  39417  pairreueq  43980  prprsprreu  43989  prprreueq  43990
  Copyright terms: Public domain W3C validator