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 3145
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 3143). (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 3140 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2649 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 207 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  reuanid  3328  nfreu1  3371  nfreud  3373  nfreuw  3375  reubida  3388  reubidva  3389  reubiia  3391  reueq1f  3400  reueq1  3408  reu5  3431  rmo5  3435  reueubd  3437  cbvreuw  3444  cbvreu  3448  reuv  3522  reu2  3715  reu6  3716  reu3  3717  2reuswap  3736  2reuswap2  3737  2reu5lem1  3745  cbvreucsf  3926  reuss2  4282  reuun2  4285  reupick  4286  reupick3  4287  euelss  4289  reusn  4657  rabsneu  4659  reusv2lem4  5293  reusv2lem5  5294  reuhypd  5311  funcnv3  6418  feu  6548  dff4  6860  f1ompt  6868  fsn  6890  riotauni  7109  riotacl2  7119  riota1  7124  riota1a  7125  riota2df  7126  snriota  7136  riotaund  7142  aceq1  9532  dfac2b  9545  nqerf  10341  zmin  12333  climreu  14903  divalglem10  15743  divalgb  15745  uptx  22163  txcn  22164  q1peqb  24677  axcontlem2  26679  edgnbusgreu  27077  nbusgredgeu0  27078  frgr3vlem2  27981  3vfriswmgrlem  27984  frgrncvvdeqlem2  28007  adjeu  29594  reuxfrdf  30183  rmoxfrd  30185  neibastop3  33608  cbvreud  34537  poimirlem25  34799  poimirlem27  34801  pairreueq  43519  prprsprreu  43528  prprreueq  43529
  Copyright terms: Public domain W3C validator