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

Definition df-rex 2765
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 2760 . 2
52cv 1669 . . . . 5
65, 3wcel 1732 . . . 4
76, 1wa 360 . . 3
87, 2wex 1565 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  ralnex  2769  rexnal  2770  rexbida  2774  rexbidv2  2782  rexbii2  2788  r2exf  2795  risset  2807  nfre1  2816  rexex  2819  rspe  2821  rsp2e  2823  reximi2  2866  reximdv2  2869  r19.23t  2874  r19.41  2915  reean  2930  rexeqf  2957  reu5  2979  rmo5  2982  cbvrexdva2  2995  rexv  3029  2gencl  3044  3gencl  3045  rspce  3108  ceqsrexv  3131  rexab  3160  rexab2  3164  rexrab2  3165  morex  3181  reu2  3185  reu6  3186  reu3  3187  2reuswap  3199  2reu5lem3  3204  2reu5  3205  rexun  3573  reuss2  3666  reuun2  3669  reupick  3670  reupick3  3671  reximdva0  3684  rabn0  3692  r19.2z  3803  r19.2zb  3804  rexsns  3942  rexsnsOLD  3943  exsnrex  3946  dfuni2  4119  eluni2  4121  elunirab  4129  iuncom4  4204  iunxiun  4279  intexrab  4474  reusv5OLD  4525  elxp2  4880  opeliunxp  4912  xpiundi  4915  xpiundir  4916  dmuni  5071  rnmpt  5107  elrnmpt1  5110  elres  5168  dfima2  5194  dfima3  5195  elima2  5198  dfco2a  5358  imaco  5363  dffo4  5875  dffo5  5876  abrexco  5975  isomin  6038  zfrep6  6552  opabex3d  6561  opabex3  6562  abexssex  6565  abexex  6566  frxp  6688  rdglim2  6852  oarec  6967  oeeu  7008  mapsn  7218  mapsnen  7349  pssnn  7492  unblem2  7526  dffi2  7595  marypha2lem4  7610  marypha2  7611  zfregcl  7729  axinf2  7762  zfinf2  7764  rankuni  7956  scott0  7979  cp  7984  bnd2  7986  infpwfien  8114  aceq1  8169  dfac5lem2  8176  dfac5lem3  8177  dfac2  8182  kmlem3  8203  kmlem6  8206  kmlem8  8208  kmlem14  8214  infmap2  8269  ackbij2  8294  cfub  8300  cfval2  8311  cflim3  8313  cfss  8316  cfslb  8317  isf32lem9  8412  zorn2lem6  8552  iundom2g  8586  winalim2  8742  grothprim  8880  genpass  9057  nqpr  9062  1idpr  9077  ltexprlem4  9087  ltexprlem5  9088  reclem2pr  9096  axrrecex  9209  sup2  10152  infm3  10155  nnunb  10441  2rexuz  10771  nnwos  10786  xrsupsslem  11133  xrinfmsslem  11134  cshwsexa  12305  maxprmfct  13646  vdwapun  13882  vdwmc  13886  vdwmc2  13887  ram0  13930  imasleval  14320  mreexexlem2d  14424  isssc  14574  drsdirfi  14949  dirge  15248  odcau  15847  ablfac2  16262  lspprat  16848  lidlnz  16924  psgnunilem4  17650  isbasis2g  18027  tgval2  18035  ntreq0  18155  neitr  18258  cmpfi  18485  is1stc2  18520  2ndcsb  18527  2ndcsep  18537  1stcelcls  18539  hausmapdom  18578  isfbas2  18882  fbssint  18885  isfil2  18903  elfg  18918  fgcl  18925  uffix2  18971  alexsubALTlem4  19096  lpbl  19548  metustexhalfOLD  19608  metustexhalf  19609  metuel2  19624  restmetu  19632  bcthlem5  20296  umgraex  22379  usgraedg4  22427  uvtx01vtx  22522  3v3e3cycl2  22672  ubthlem1  23393  axhcompl-zf  23522  isch3  23766  shne0i  23973  cnlnssadj  24606  2reuswap2  25000  rexunirn  25003  rmoxfrdOLD  25004  rmoxfrd  25005  abrexdomjm  25016  abrexexd  25018  fpwrelmapffslem  25162  ishashinf  25215  ordtconlem1  25533  ddemeas  25832  eulerpartlemgvv  25933  erdszelem10  26234  ptpcon  26268  dedekind  26526  coep  26713  coepr  26714  dffr5  26715  dfpo2  26717  opelco3  26742  dfon2lem8  26756  brimg  27121  dfrdg4  27134  tfrqfree  27135  ellines  27425  neifg  27772  abrexdom  27804  prdstotbnd  27875  n0el  28148  prtlem17  28165  prter2  28170  rexbidar  28876  ssrexf  28910  rspcegf  28920  cncmpmax  28929  rfcnnnub  28933  stoweidlem14  28988  stoweidlem27  29001  stoweidlem34  29008  stoweidlem35  29009  stoweidlem43  29017  stoweidlem44  29018  stoweidlem50  29024  stoweidlem54  29028  stoweidlem56  29030  stoweidlem59  29033  stoweidlem60  29034  2rmoswap  29187  wwlktovfo  29434  wlknwwlknsur  29525  wlkiswwlksur  29532  wwlkextsur  29544  frisusgranb  29770  frgra3vlem2  29774  3vfriswmgralem  29777  frgrancvvdeqlemC  29813  usg2spot2nb  29839  onfrALTlem5  30096  onfrALTlem2  30100  onfrALTlem1  30102  onfrALTlem5VD  30467  onfrALTlem2VD  30471  onfrALTlem1VD  30472  chordthmALT  30515  bnj168  30567  bnj956  30617  bnj1098  30624  bnj1143  30631  bnj1146  30632  bnj1185  30635  bnj1196  30636  bnj600  30760  bnj849  30766  bnj906  30771  bnj916  30774  bnj983  30792  bnj984  30793  bnj1083  30817  bnj1176  30844  bnj1186  30846  bnj1189  30848  bnj1228  30850  bnj1253  30856  bnj1398  30873  bnj1463  30894  bnj1312  30897  bnj1514  30902  bj-snglc  30952  bj-snglss  30953  islshpat  31365  lsat0cv  31381  lshpsmreu  31457  atex  31753  islpln5  31882  islvol5  31926  pmapglb  32117  pmapglb2N  32118  pmapglb2xN  32119  elpaddn0  32147  pmapjat1  32200  polval2N  32253  osumcllem11N  32313  pexmidlem8N  32324  cdlemftr3  32912  dibelval3  33495  dibglbN  33514  dicelval3  33528  dihglbcpreN  33648  dihglb2  33690  dihjatcclem4  33769  mapdordlem2  33985  mapdrvallem2  33993  mapdpglem3  34023  hdmapglem7a  34278
  Copyright terms: Public domain W3C validator