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

Definition df-rex 2813
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 2808 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wa 369 . . 3
87, 2wex 1612 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2903  rexnalOLD  2906  rexex  2914  rspe  2915  rsp2eOLD  2917  nfre1  2918  reximi2  2924  reximd2a  2927  reximdv2  2928  r19.23t  2935  rexbii2  2957  rexbida  2963  rexbidv2  2964  r2exfOLD  2979  risset  2982  r19.41v  3009  r19.41  3010  reean  3024  rexeqf  3051  reu5  3073  rmo5  3076  cbvrexdva2  3089  rexv  3124  2gencl  3140  3gencl  3141  rspce  3205  ceqsrexv  3233  rexab  3262  rexab2  3266  rexrab2  3267  morex  3283  reu2  3287  reu6  3288  reu3  3289  2reuswap  3302  2reu5lem3  3307  2reu5  3308  rexun  3683  reuss2  3777  reuun2  3780  reupick  3781  reupick3  3782  reximdva0  3796  rabn0  3805  r19.2z  3918  r19.2zb  3919  rexsns  4062  rexsnsOLD  4063  exsnrex  4067  dfuni2  4251  eluni2  4253  elunirab  4261  iuncom4  4338  iunxiun  4413  intexrab  4611  reusv5OLD  4662  elxp2  5022  opeliunxp  5056  xpiundi  5059  xpiundir  5060  dmuni  5217  rnmpt  5253  elrnmpt1  5256  elres  5314  dfima2  5344  dfima3  5345  elima2  5348  dfco2a  5512  imaco  5517  dffo4  6047  dffo5  6048  abrexco  6156  isomin  6233  zfrep6  6768  opabex3d  6778  opabex3  6779  abexssex  6782  abexex  6783  frxp  6910  rdglim2  7117  oarec  7230  oeeu  7271  mapsn  7480  mapsnen  7613  pssnn  7758  unblem2  7793  dffi2  7903  marypha2lem4  7918  marypha2  7919  zfregcl  8041  axinf2  8078  zfinf2  8080  rankuni  8302  scott0  8325  cp  8330  bnd2  8332  infpwfien  8464  aceq1  8519  dfac5lem2  8526  dfac5lem3  8527  dfac2  8532  kmlem3  8553  kmlem6  8556  kmlem8  8558  kmlem14  8564  infmap2  8619  ackbij2  8644  cfub  8650  cfval2  8661  cflim3  8663  cfss  8666  cfslb  8667  isf32lem9  8762  zorn2lem6  8902  iundom2g  8936  winalim2  9095  grothprim  9233  genpass  9408  nqpr  9413  1idpr  9428  ltexprlem4  9438  ltexprlem5  9439  reclem2pr  9447  axrrecex  9561  dedekind  9765  sup2  10524  infm3  10527  nnunb  10816  2rexuz  11162  nnwos  11178  xrsupsslem  11527  xrinfmsslem  11528  cshwsexa  12792  wwlktovfo  12896  maxprmfct  14254  vdwapun  14492  vdwmc  14496  vdwmc2  14497  ram0  14540  imasleval  14938  mreexexlem2d  15042  isssc  15189  drsdirfi  15567  dirge  15867  psgnunilem4  16522  odcau  16624  ablfac2  17140  lspprat  17799  lidlnz  17876  isbasis2g  19449  tgval2  19457  ntreq0  19578  neitr  19681  cmpfi  19908  is1stc2  19943  2ndcsb  19950  2ndcsep  19960  1stcelcls  19962  hausmapdom  20001  isfbas2  20336  fbssint  20339  isfil2  20357  elfg  20372  fgcl  20379  uffix2  20425  alexsubALTlem4  20550  lpbl  21006  metustexhalfOLD  21066  metustexhalf  21067  metuel2  21082  restmetu  21090  bcthlem5  21767  umgraex  24323  usgraedg4  24387  uvtx01vtx  24492  3v3e3cycl2  24664  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  frisusgranb  24997  frgra3vlem2  25001  3vfriswmgralem  25004  frgrancvvdeqlemC  25039  usg2spot2nb  25065  ubthlem1  25786  axhcompl-zf  25915  isch3  26159  shne0i  26366  cnlnssadj  26999  2reuswap2  27387  rexunirn  27390  rmoxfrdOLD  27391  rmoxfrd  27392  abrexdomjm  27405  abrexexd  27407  fpwrelmapffslem  27555  ishashinf  27606  ordtconlem1  27906  ddemeas  28208  eulerpartlemgvv  28315  erdszelem10  28644  ptpcon  28678  coep  29180  coepr  29181  dffr5  29182  dfpo2  29184  opelco3  29208  dfon2lem8  29222  brimg  29587  dfrdg4  29600  tfrqfree  29601  ellines  29802  neifg  30189  abrexdom  30221  prdstotbnd  30290  n0el  30600  prtlem17  30617  prter2  30622  rexbidar  31355  ssrexf  31388  rspcegf  31398  cncmpmax  31407  rfcnnnub  31411  suprnmpt  31451  ssfiunibd  31509  islpcn  31645  lptre2pt  31646  stoweidlem14  31796  stoweidlem34  31816  stoweidlem35  31817  stoweidlem43  31825  stoweidlem44  31826  stoweidlem50  31832  stoweidlem54  31836  stoweidlem56  31838  stoweidlem59  31841  stoweidlem60  31842  fourier2  32010  2rmoswap  32189  euelss  32553  dfiso2  32568  opeliun2xp  32922  onfrALTlem5  33314  onfrALTlem2  33318  onfrALTlem1  33320  onfrALTlem5VD  33685  onfrALTlem2VD  33689  onfrALTlem1VD  33690  chordthmALT  33733  bnj168  33785  bnj956  33835  bnj1098  33842  bnj1143  33849  bnj1146  33850  bnj1185  33852  bnj1196  33853  bnj600  33977  bnj849  33983  bnj906  33988  bnj916  33991  bnj983  34009  bnj984  34010  bnj1083  34034  bnj1176  34061  bnj1186  34063  bnj1189  34065  bnj1228  34067  bnj1253  34073  bnj1398  34090  bnj1463  34111  bnj1312  34114  bnj1514  34119  bj-rexvwv  34442  bj-rexcom4  34445  bj-snglc  34527  bj-snglss  34528  bj-finsumval0  34663  islshpat  34742  lsat0cv  34758  lshpsmreu  34834  atex  35130  islpln5  35259  islvol5  35303  pmapglb  35494  pmapglb2N  35495  pmapglb2xN  35496  elpaddn0  35524  pmapjat1  35577  polval2N  35630  osumcllem11N  35690  pexmidlem8N  35701  cdlemftr3  36291  dibelval3  36874  dibglbN  36893  dicelval3  36907  dihglbcpreN  37027  dihglb2  37069  dihjatcclem4  37148  mapdordlem2  37364  mapdrvallem2  37372  mapdpglem3  37402  hdmapglem7a  37657  rp-isfinite5  37743  rp-isfinite6  37744  elintima  37765
  Copyright terms: Public domain W3C validator