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

Definition df-reu 2719
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 set 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wreu 2714 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1653 . . . . 5 class 𝑥
65, 3wcel 1728 . . . 4 wff 𝑥𝐴
76, 1wa 360 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2288 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 178 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2885  nfreud  2887  reubida  2897  reubiia  2900  reueq1f  2909  reu5  2930  rmo5  2933  cbvreu  2939  reuv  2980  reu2  3131  reu6  3132  reu3  3133  2reuswap  3145  2reu5lem1  3148  cbvreucsf  3302  reuss2  3609  reuun2  3612  reupick  3613  reupick3  3614  reusn  3906  rabsneu  3908  reusv2lem4  4762  reusv2lem5  4763  reusv6OLD  4769  reusv7OLD  4770  reuhypd  4785  funcnv3  5547  feu  5654  dff4  5919  f1ompt  5927  fsn  5942  riotaeqdv  6586  riotauni  6592  riotacl2  6599  riota1  6604  riota1a  6605  riota2df  6606  snriota  6616  riotaprc  6623  aceq1  8036  dfac2  8049  nqerf  8845  zmin  10608  climreu  12388  divalglem10  12960  divalgb  12962  uptx  17695  txcn  17696  q1peqb  20115  adjeu  23430  2reuswap2  24011  rmoxfrdOLD  24015  rmoxfrd  24016  axcontlem2  25939  neibastop3  26433  frgra3vlem2  28563  3vfriswmgralem  28566  frgrancvvdeqlem3  28593  frgraeu  28615
  Copyright terms: Public domain W3C validator