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

Definition df-rex 2718
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
2 vx . . 3
3 cA . . 3
41, 2, 3wrex 2713 . 2
52cv 1653 . . . . 5
65, 3wcel 1728 . . . 4
76, 1wa 360 . . 3
87, 2wex 1551 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  ralnex  2722  rexnal  2723  rexbida  2727  rexbidv2  2735  rexbii2  2741  r2exf  2748  risset  2760  nfre1  2769  rexex  2772  rspe  2774  rsp2e  2776  reximi2  2819  reximdv2  2822  r19.23t  2827  r19.41  2867  reean  2881  rexeqf  2908  reu5  2930  rmo5  2933  cbvrexdva2  2946  rexv  2979  2gencl  2994  3gencl  2995  rspce  3056  ceqsrexv  3078  rexab  3106  rexab2  3110  rexrab2  3111  morex  3127  reu2  3131  reu6  3132  reu3  3133  2reuswap  3145  2reu5lem3  3150  2reu5  3151  rexun  3516  reuss2  3609  reuun2  3612  reupick  3613  reupick3  3614  reximdva0  3627  rabn0  3635  r19.2z  3743  r19.2zb  3744  rexsns  3872  rexsnsOLD  3873  exsnrex  3876  dfuni2  4045  eluni2  4047  elunirab  4055  iuncom4  4129  iunxiun  4204  intexrab  4398  reusv5OLD  4774  elxp2  4937  opeliunxp  4969  xpiundi  4972  xpiundir  4973  dmuni  5123  rnmpt  5159  elrnmpt1  5162  elres  5225  dfima2  5249  dfima3  5250  elima2  5253  dfco2a  5416  imaco  5421  dffo4  5933  dffo5  5934  zfrep6  6016  abrexco  6034  opabex3d  6037  opabex3  6038  abexssex  6050  abexex  6051  isomin  6105  frxp  6506  rdglim2  6739  oarec  6854  oeeu  6895  mapsn  7104  mapsnen  7233  pssnn  7376  unblem2  7409  dffi2  7477  marypha2lem4  7492  marypha2  7493  zfregcl  7611  axinf2  7644  zfinf2  7646  rankuni  7838  scott0  7861  cp  7866  bnd2  7868  infpwfien  7994  aceq1  8049  dfac5lem2  8056  dfac5lem3  8057  dfac2  8062  kmlem3  8083  kmlem6  8086  kmlem8  8088  kmlem14  8094  infmap2  8149  ackbij2  8174  cfub  8180  cfval2  8191  cflim3  8193  cfss  8196  cfslb  8197  isf32lem9  8292  zorn2lem6  8432  iundom2g  8466  winalim2  8622  grothprim  8760  genpass  8937  nqpr  8942  1idpr  8957  ltexprlem4  8967  ltexprlem5  8968  reclem2pr  8976  axrrecex  9089  sup2  10015  infm3  10018  nnunb  10268  2rexuz  10580  nnwos  10595  xrsupsslem  10936  xrinfmsslem  10937  maxprmfct  13164  vdwapun  13393  vdwmc  13397  vdwmc2  13398  ram0  13441  imasleval  13817  mreexexlem2d  13921  isssc  14071  drsdirfi  14446  dirge  14733  odcau  15289  ablfac2  15698  lspprat  16276  lidlnz  16350  isbasis2g  17064  tgval2  17072  ntreq0  17192  neitr  17295  cmpfi  17522  is1stc2  17556  2ndcsb  17563  2ndcsep  17573  1stcelcls  17575  hausmapdom  17614  isfbas2  17918  fbssint  17921  isfil2  17939  elfg  17954  fgcl  17961  uffix2  18007  alexsubALTlem4  18132  lpbl  18584  metustexhalfOLD  18644  metustexhalf  18645  metuel2  18660  restmetu  18668  bcthlem5  19332  umgraex  21409  usgraedg4  21457  uvtx01vtx  21552  3v3e3cycl2  21702  ubthlem1  22423  axhcompl-zf  22552  isch3  22795  shne0i  23001  cnlnssadj  23634  2reuswap2  24024  rexunirn  24027  rmoxfrdOLD  24028  rmoxfrd  24029  abrexdomjm  24037  abrexexd  24039  ishashinf  24208  fpwrelmapffslem  24736  eulerpartlemgvv  24762  erdszelem10  24990  ptpcon  25024  dedekind  25291  coep  25478  coepr  25479  dffr5  25480  dfpo2  25482  opelco3  25507  dfon2lem8  25521  brimg  25886  dfrdg4  25899  tfrqfree  25900  ellines  26190  neifg  26511  abrexdom  26543  prdstotbnd  26614  n0el  26889  prtlem17  26906  prter2  26911  psgnunilem4  27576  rexbidar  27804  ssrexf  27838  rspcegf  27848  cncmpmax  27857  rfcnnnub  27861  stoweidlem14  27917  stoweidlem27  27930  stoweidlem34  27937  stoweidlem35  27938  stoweidlem43  27946  stoweidlem44  27947  stoweidlem50  27953  stoweidlem54  27957  stoweidlem56  27959  stoweidlem59  27962  stoweidlem60  27963  2rmoswap  28116  cshwsexa  28489  frisusgranb  28625  frgra3vlem2  28629  3vfriswmgralem  28632  frgrancvvdeqlemC  28666  usg2spot2nb  28692  onfrALTlem5  28867  onfrALTlem2  28871  onfrALTlem1  28873  onfrALTlem5VD  29238  onfrALTlem2VD  29242  onfrALTlem1VD  29243  chordthmALT  29286  bnj168  29338  bnj956  29388  bnj1098  29395  bnj1143  29402  bnj1146  29403  bnj1185  29406  bnj1196  29407  bnj600  29531  bnj849  29537  bnj906  29542  bnj916  29545  bnj983  29563  bnj984  29564  bnj1083  29588  bnj1176  29615  bnj1186  29617  bnj1189  29619  bnj1228  29621  bnj1253  29627  bnj1398  29644  bnj1463  29665  bnj1312  29668  bnj1514  29673  islshpat  30055  lsat0cv  30071  lshpsmreu  30147  atex  30443  islpln5  30572  islvol5  30616  pmapglb  30807  pmapglb2N  30808  pmapglb2xN  30809  elpaddn0  30837  pmapjat1  30890  polval2N  30943  osumcllem11N  31003  pexmidlem8N  31014  cdlemftr3  31602  dibelval3  32185  dibglbN  32204  dicelval3  32218  dihglbcpreN  32338  dihglb2  32380  dihjatcclem4  32459  mapdordlem2  32675  mapdrvallem2  32683  mapdpglem3  32713  hdmapglem7a  32968
  Copyright terms: Public domain W3C validator