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

Definition df-rex 2703
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  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
3 cA . . 3  class  A
41, 2, 3wrex 2698 . 2  wff  E. x  e.  A  ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1550 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 177 1  wff  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
Colors of variables: wff set class
This definition is referenced by:  ralnex  2707  rexnal  2708  rexbida  2712  rexbidv2  2720  rexbii2  2726  r2exf  2733  risset  2745  nfre1  2754  rexex  2757  rspe  2759  rsp2e  2761  reximi2  2804  reximdv2  2807  r19.23t  2812  r19.41  2852  reean  2866  rexeqf  2893  reu5  2913  rmo5  2916  cbvrexdva2  2929  rexv  2962  2gencl  2977  3gencl  2978  rspce  3039  ceqsrexv  3061  rexab  3089  rexab2  3093  rexrab2  3094  morex  3110  reu2  3114  reu6  3115  reu3  3116  2reuswap  3128  2reu5lem3  3133  2reu5  3134  rexun  3519  reuss2  3613  reuun2  3616  reupick  3617  reupick3  3618  reximdva0  3631  rabn0  3639  r19.2z  3709  r19.2zb  3710  rexsns  3837  exsnrex  3840  dfuni2  4009  eluni2  4011  elunirab  4020  iuncom4  4092  iunxiun  4165  intexrab  4351  reusv5OLD  4725  elxp2  4888  opeliunxp  4921  xpiundi  4924  xpiundir  4925  dmuni  5071  rnmpt  5108  elrnmpt1  5111  elres  5173  dfima2  5197  dfima3  5198  elima2  5201  dfco2a  5362  imaco  5367  dffo4  5877  dffo5  5878  zfrep6  5960  abrexco  5978  opabex3d  5981  opabex3  5982  abexssex  5994  abexex  5995  isomin  6049  frxp  6448  rdglim2  6682  oarec  6797  oeeu  6838  mapsn  7047  mapsnen  7176  pssnn  7319  unblem2  7352  dffi2  7420  marypha2lem4  7435  marypha2  7436  zfregcl  7554  axinf2  7587  zfinf2  7589  rankuni  7781  scott0  7802  cp  7807  bnd2  7809  infpwfien  7935  aceq1  7990  dfac5lem2  7997  dfac5lem3  7998  dfac2  8003  kmlem3  8024  kmlem6  8027  kmlem8  8029  kmlem14  8035  infmap2  8090  ackbij2  8115  cfub  8121  cfval2  8132  cflim3  8134  cfss  8137  cfslb  8138  isf32lem9  8233  zorn2lem6  8373  iundom2g  8407  winalim2  8563  grothprim  8701  genpass  8878  nqpr  8883  1idpr  8898  ltexprlem4  8908  ltexprlem5  8909  reclem2pr  8917  axrrecex  9030  sup2  9956  infm3  9959  nnunb  10209  2rexuz  10521  nnwos  10536  xrsupsslem  10877  xrinfmsslem  10878  maxprmfct  13105  vdwapun  13334  vdwmc  13338  vdwmc2  13339  ram0  13382  imasleval  13758  mreexexlem2d  13862  isssc  14012  drsdirfi  14387  dirge  14674  odcau  15230  ablfac2  15639  lspprat  16217  lidlnz  16291  isbasis2g  17005  tgval2  17013  ntreq0  17133  neitr  17236  cmpfi  17463  is1stc2  17497  2ndcsb  17504  2ndcsep  17514  1stcelcls  17516  hausmapdom  17555  isfbas2  17859  fbssint  17862  isfil2  17880  elfg  17895  fgcl  17902  uffix2  17948  alexsubALTlem4  18073  lpbl  18525  metustexhalfOLD  18585  metustexhalf  18586  metuel2  18601  restmetu  18609  bcthlem5  19273  umgraex  21350  usgraedg4  21398  uvtx01vtx  21493  3v3e3cycl2  21643  ubthlem1  22364  axhcompl-zf  22493  isch3  22736  shne0i  22942  cnlnssadj  23575  2reuswap2  23967  rexunirn  23970  rmoxfrdOLD  23971  rmoxfrd  23972  abrexdomjm  23980  abrexexd  23982  ishashinf  24151  erdszelem10  24878  ptpcon  24912  dedekind  25179  coep  25366  coepr  25367  dffr5  25368  dfpo2  25370  opelco3  25395  dfon2lem8  25409  brimg  25774  dfrdg4  25787  tfrqfree  25788  ellines  26078  neifg  26391  abrexdom  26423  prdstotbnd  26494  n0el  26699  prtlem17  26716  prter2  26721  psgnunilem4  27388  rexbidar  27616  ssrexf  27651  rspcegf  27661  cncmpmax  27670  rfcnnnub  27674  stoweidlem14  27730  stoweidlem27  27743  stoweidlem34  27750  stoweidlem35  27751  stoweidlem43  27759  stoweidlem44  27760  stoweidlem50  27766  stoweidlem54  27770  stoweidlem56  27772  stoweidlem59  27775  stoweidlem60  27776  2rmoswap  27929  cshwsexa  28254  frisusgranb  28324  frgra3vlem2  28328  3vfriswmgralem  28331  frgrancvvdeqlemC  28365  usg2spot2nb  28391  onfrALTlem5  28565  onfrALTlem2  28569  onfrALTlem1  28571  onfrALTlem5VD  28934  onfrALTlem2VD  28938  onfrALTlem1VD  28939  chordthmALT  28982  bnj168  29034  bnj956  29084  bnj1098  29091  bnj1143  29098  bnj1146  29099  bnj1185  29102  bnj1196  29103  bnj600  29227  bnj849  29233  bnj906  29238  bnj916  29241  bnj983  29259  bnj984  29260  bnj1083  29284  bnj1176  29311  bnj1186  29313  bnj1189  29315  bnj1228  29317  bnj1253  29323  bnj1398  29340  bnj1463  29361  bnj1312  29364  bnj1514  29369  islshpat  29752  lsat0cv  29768  lshpsmreu  29844  atex  30140  islpln5  30269  islvol5  30313  pmapglb  30504  pmapglb2N  30505  pmapglb2xN  30506  elpaddn0  30534  pmapjat1  30587  polval2N  30640  osumcllem11N  30700  pexmidlem8N  30711  cdlemftr3  31299  dibelval3  31882  dibglbN  31901  dicelval3  31915  dihglbcpreN  32035  dihglb2  32077  dihjatcclem4  32156  mapdordlem2  32372  mapdrvallem2  32380  mapdpglem3  32410  hdmapglem7a  32665
  Copyright terms: Public domain W3C validator