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

Definition df-reu 2755
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 2750 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1661 . . . . 5 class 𝑥
65, 3wcel 1734 . . . 4 wff 𝑥𝐴
76, 1wa 360 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2321 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 178 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfreu1  2922  nfreud  2924  reubida  2934  reubiia  2937  reueq1f  2946  reu5  2967  rmo5  2970  cbvreu  2976  reuv  3018  reu2  3170  reu6  3171  reu3  3172  2reuswap  3184  2reu5lem1  3187  cbvreucsf  3343  reuss2  3650  reuun2  3653  reupick  3654  reupick3  3655  reusn  3954  rabsneu  3956  reusv2lem4  4819  reusv2lem5  4820  reusv6OLD  4826  reusv7OLD  4827  reuhypd  4842  funcnv3  5611  feu  5718  dff4  5983  f1ompt  5991  fsn  6006  riotauni  6661  riotacl2  6669  riota1  6674  riota1a  6675  riota2df  6676  snriota  6685  riotaund  6691  aceq1  8095  dfac2  8108  nqerf  8904  zmin  10670  climreu  12470  divalglem10  13042  divalgb  13044  uptx  17789  txcn  17790  q1peqb  20209  adjeu  23524  2reuswap2  24109  rmoxfrdOLD  24113  rmoxfrd  24114  axcontlem2  26361  neibastop3  26847  frgra3vlem2  29288  3vfriswmgralem  29291  frgrancvvdeqlem3  29320  frgraeu  29342
  Copyright terms: Public domain W3C validator