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

Definition df-rex 2914
Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
df-rex (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrex 2909 . 2 wff 𝑥𝐴 𝜑
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1701 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2988  ralnexOLD  2989  rexex  2998  rspe  2999  nfre1  3001  reximi2  3006  reximd2a  3009  reximdv2  3010  r19.23t  3016  rexbii2  3034  rexbida  3042  rexbidv2  3043  risset  3057  r19.41v  3083  r19.41  3084  reean  3100  rexeqf  3128  reu5  3152  rmo5  3155  cbvrexdva2  3168  rexv  3210  2gencl  3226  3gencl  3227  rspce  3294  ceqsrexv  3324  rexab  3356  rexab2  3360  rexrab2  3361  morex  3377  reu2  3381  reu6  3382  reu3  3383  2reuswap  3397  2reu5lem3  3402  2reu5  3403  ssrexf  3650  rexun  3777  reuss2  3889  reuun2  3892  reupick  3893  reupick3  3894  euelss  3896  reximdva0  3915  n0rex  3917  rabn0OLD  3939  r19.2z  4038  r19.2zb  4039  rexsns  4195  exsnrex  4199  dfuni2  4411  eluni2  4413  elunirab  4421  iuncom4  4501  iunxiun  4581  intexrab  4793  elxp2OLD  5103  opeliunxp  5141  xpiundi  5144  xpiundir  5145  ssrelrn  5285  dmuni  5304  rnmpt  5341  elrnmpt1  5344  elres  5404  dfima2  5437  dfima3  5438  elima2  5441  dfco2a  5604  imaco  5609  elsnxp  5646  elsnxpOLD  5647  dffo4  6341  dffo5  6342  abrexco  6467  isomin  6552  zfrep6  7096  opabex3d  7106  opabex3  7107  abexssex  7110  abexex  7111  frxp  7247  dfrecs3  7429  rdglim2  7488  oarec  7602  oeeu  7643  mapsn  7859  mapsnen  7995  pssnn  8138  unblem2  8173  dffi2  8289  marypha2lem4  8304  marypha2  8305  zfregcl  8459  zfregclOLD  8461  axinf2  8497  zfinf2  8499  rankuni  8686  scott0  8709  cp  8714  bnd2  8716  infpwfien  8845  aceq1  8900  dfac5lem2  8907  dfac5lem3  8908  dfac2  8913  kmlem3  8934  kmlem6  8937  kmlem8  8939  kmlem14  8945  infmap2  9000  ackbij2  9025  cfub  9031  cfval2  9042  cflim3  9044  cfss  9047  cfslb  9048  isf32lem9  9143  zorn2lem6  9283  iundom2g  9322  winalim2  9478  grothprim  9616  genpass  9791  nqpr  9796  1idpr  9811  ltexprlem4  9821  ltexprlem5  9822  reclem2pr  9830  axrrecex  9944  dedekind  10160  sup2  10939  infm3  10942  nnunb  11248  2rexuz  11700  nnwos  11715  xrsupsslem  12096  xrinfmsslem  12097  ishashinf  13201  cshwsexa  13523  wwlktovfo  13651  ncoprmgcdne1b  15306  maxprmfct  15364  vdwapun  15621  vdwmc  15625  vdwmc2  15626  ram0  15669  imasleval  16141  mreexexlem2d  16245  dfiso2  16372  isssc  16420  drsdirfi  16878  dirge  17177  psgnunilem4  17857  odcau  17959  ablfac2  18428  lspprat  19093  lidlnz  19168  isbasis2g  20692  tgval2  20700  ntreq0  20821  neitr  20924  cmpfi  21151  is1stc2  21185  2ndcsb  21192  2ndcsep  21202  1stcelcls  21204  hausmapdom  21243  isfbas2  21579  fbssint  21582  isfil2  21600  elfg  21615  fgcl  21622  uffix2  21668  alexsubALTlem4  21794  lpbl  22248  metustexhalf  22301  metuel2  22310  restmetu  22315  bcthlem5  23065  upgrex  25917  uvtxa01vtx0  26218  uhgrvd00  26350  wlkpwwlkf1ouspgr  26668  wlknwwlksnsur  26679  wlkwwlksur  26686  wwlksnextsur  26698  frcond3  27032  frgr3vlem2  27036  3vfriswmgrlem  27039  frgrncvvdeqlemC  27070  fusgr2wsp2nb  27090  ubthlem1  27614  axhcompl-zf  27743  isch3  27986  shne0i  28195  cnlnssadj  28827  2reuswap2  29217  rexunirn  29220  rmoxfrdOLD  29221  rmoxfrd  29222  abrexdomjm  29233  abrexexd  29235  1stpreimas  29367  fpwrelmapffslem  29391  ordtconnlem1  29794  ddemeas  30122  omssubaddlem  30184  omssubadd  30185  eulerpartlemgvv  30261  bnj168  30559  bnj956  30608  bnj1098  30615  bnj1143  30622  bnj1146  30623  bnj1185  30625  bnj1196  30626  bnj600  30750  bnj849  30756  bnj906  30761  bnj916  30764  bnj983  30782  bnj984  30783  bnj1083  30807  bnj1176  30834  bnj1186  30836  bnj1189  30838  bnj1228  30840  bnj1253  30846  bnj1398  30863  bnj1463  30884  bnj1312  30887  bnj1514  30892  erdszelem10  30943  ptpconn  30976  coep  31402  coepr  31403  dffr5  31404  dfpo2  31406  opelco3  31433  dfon2lem8  31449  brimg  31739  dfrecs2  31752  dfrdg4  31753  ellines  31954  neifg  32061  bj-rexvwv  32566  bj-rexcom4  32569  bj-snglc  32657  bj-snglss  32658  bj-rest10  32731  bj-restn0  32733  bj-restpw  32735  bj-rest0  32736  bj-restb  32737  bj-restuni  32740  bj-dfmpt2a  32747  bj-finsumval0  32819  rnmptsn  32853  f1omptsnlem  32854  mptsnunlem  32856  topdifinffinlem  32866  isbasisrelowllem1  32874  isbasisrelowllem2  32875  relowlpssretop  32883  poimirlem30  33110  abrexdom  33196  prdstotbnd  33264  n0el  33665  prtlem17  33680  prter2  33685  islshpat  33823  lsat0cv  33839  lshpsmreu  33915  atex  34211  islpln5  34340  islvol5  34384  pmapglb  34575  pmapglb2N  34576  pmapglb2xN  34577  elpaddn0  34605  pmapjat1  34658  polval2N  34711  osumcllem11N  34771  pexmidlem8N  34782  cdlemftr3  35372  dibelval3  35955  dibglbN  35974  dicelval3  35988  dihglbcpreN  36108  dihglb2  36150  dihjatcclem4  36229  mapdordlem2  36445  mapdrvallem2  36453  mapdpglem3  36483  hdmapglem7a  36738  rp-isfinite5  37383  rp-isfinite6  37384  relintabex  37407  elintima  37465  iunrelexpuztr  37531  cotrclrcl  37554  neik0pk1imk0  37866  ntrneineine0lem  37902  ntrneineine1lem  37903  ntrneiel2  37905  rexbidar  38171  onfrALTlem5  38278  onfrALTlem2  38282  onfrALTlem1  38284  onfrALTlem5VD  38643  onfrALTlem2VD  38647  onfrALTlem1VD  38648  chordthmALT  38691  rspcegf  38704  cncmpmax  38713  rfcnnnub  38717  inn0f  38764  nssrex  38782  eluni2f  38808  eliin2f  38809  suprnmpt  38864  founiiun0  38886  disjinfi  38889  mapsnd  38897  mapsnend  38900  ssfiunibd  39022  infrpge  39066  fsumiunss  39243  islpcn  39307  lptre2pt  39308  stoweidlem14  39568  stoweidlem34  39588  stoweidlem35  39589  stoweidlem43  39597  stoweidlem44  39598  stoweidlem50  39604  stoweidlem54  39608  stoweidlem56  39610  stoweidlem59  39613  stoweidlem60  39614  fourier2  39781  qndenserrnbllem  39851  qndenserrn  39856  sge0rpcpnf  39975  hoidmvval0b  40141  hoiqssbllem3  40175  2rmoswap  40518  opeliun2xp  41429  setrec1lem3  41759
  Copyright terms: Public domain W3C validator