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

Definition df-rex 2717
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 2712 . 2  wff  E. x  e.  A  ph
52cv 1652 . . . . 5  class  x
65, 3wcel 1727 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1551 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 178 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  2721  rexnal  2722  rexbida  2726  rexbidv2  2734  rexbii2  2740  r2exf  2747  risset  2759  nfre1  2768  rexex  2771  rspe  2773  rsp2e  2775  reximi2  2818  reximdv2  2821  r19.23t  2826  r19.41  2866  reean  2880  rexeqf  2907  reu5  2927  rmo5  2930  cbvrexdva2  2943  rexv  2976  2gencl  2991  3gencl  2992  rspce  3053  ceqsrexv  3075  rexab  3103  rexab2  3107  rexrab2  3108  morex  3124  reu2  3128  reu6  3129  reu3  3130  2reuswap  3142  2reu5lem3  3147  2reu5  3148  rexun  3513  reuss2  3606  reuun2  3609  reupick  3610  reupick3  3611  reximdva0  3624  rabn0  3632  r19.2z  3741  r19.2zb  3742  rexsns  3869  exsnrex  3872  dfuni2  4041  eluni2  4043  elunirab  4052  iuncom4  4124  iunxiun  4198  intexrab  4388  reusv5OLD  4762  elxp2  4925  opeliunxp  4958  xpiundi  4961  xpiundir  4962  dmuni  5108  rnmpt  5145  elrnmpt1  5148  elres  5210  dfima2  5234  dfima3  5235  elima2  5238  dfco2a  5399  imaco  5404  dffo4  5914  dffo5  5915  zfrep6  5997  abrexco  6015  opabex3d  6018  opabex3  6019  abexssex  6031  abexex  6032  isomin  6086  frxp  6485  rdglim2  6719  oarec  6834  oeeu  6875  mapsn  7084  mapsnen  7213  pssnn  7356  unblem2  7389  dffi2  7457  marypha2lem4  7472  marypha2  7473  zfregcl  7591  axinf2  7624  zfinf2  7626  rankuni  7818  scott0  7841  cp  7846  bnd2  7848  infpwfien  7974  aceq1  8029  dfac5lem2  8036  dfac5lem3  8037  dfac2  8042  kmlem3  8063  kmlem6  8066  kmlem8  8068  kmlem14  8074  infmap2  8129  ackbij2  8154  cfub  8160  cfval2  8171  cflim3  8173  cfss  8176  cfslb  8177  isf32lem9  8272  zorn2lem6  8412  iundom2g  8446  winalim2  8602  grothprim  8740  genpass  8917  nqpr  8922  1idpr  8937  ltexprlem4  8947  ltexprlem5  8948  reclem2pr  8956  axrrecex  9069  sup2  9995  infm3  9998  nnunb  10248  2rexuz  10560  nnwos  10575  xrsupsslem  10916  xrinfmsslem  10917  maxprmfct  13144  vdwapun  13373  vdwmc  13377  vdwmc2  13378  ram0  13421  imasleval  13797  mreexexlem2d  13901  isssc  14051  drsdirfi  14426  dirge  14713  odcau  15269  ablfac2  15678  lspprat  16256  lidlnz  16330  isbasis2g  17044  tgval2  17052  ntreq0  17172  neitr  17275  cmpfi  17502  is1stc2  17536  2ndcsb  17543  2ndcsep  17553  1stcelcls  17555  hausmapdom  17594  isfbas2  17898  fbssint  17901  isfil2  17919  elfg  17934  fgcl  17941  uffix2  17987  alexsubALTlem4  18112  lpbl  18564  metustexhalfOLD  18624  metustexhalf  18625  metuel2  18640  restmetu  18648  bcthlem5  19312  umgraex  21389  usgraedg4  21437  uvtx01vtx  21532  3v3e3cycl2  21682  ubthlem1  22403  axhcompl-zf  22532  isch3  22775  shne0i  22981  cnlnssadj  23614  2reuswap2  24006  rexunirn  24009  rmoxfrdOLD  24010  rmoxfrd  24011  abrexdomjm  24019  abrexexd  24021  ishashinf  24190  erdszelem10  24917  ptpcon  24951  dedekind  25218  coep  25405  coepr  25406  dffr5  25407  dfpo2  25409  opelco3  25434  dfon2lem8  25448  brimg  25813  dfrdg4  25826  tfrqfree  25827  ellines  26117  neifg  26438  abrexdom  26470  prdstotbnd  26541  n0el  26746  prtlem17  26763  prter2  26768  psgnunilem4  27435  rexbidar  27663  ssrexf  27698  rspcegf  27708  cncmpmax  27717  rfcnnnub  27721  stoweidlem14  27777  stoweidlem27  27790  stoweidlem34  27797  stoweidlem35  27798  stoweidlem43  27806  stoweidlem44  27807  stoweidlem50  27813  stoweidlem54  27817  stoweidlem56  27819  stoweidlem59  27822  stoweidlem60  27823  2rmoswap  27976  cshwsexa  28349  frisusgranb  28485  frgra3vlem2  28489  3vfriswmgralem  28492  frgrancvvdeqlemC  28526  usg2spot2nb  28552  onfrALTlem5  28726  onfrALTlem2  28730  onfrALTlem1  28732  onfrALTlem5VD  29095  onfrALTlem2VD  29099  onfrALTlem1VD  29100  chordthmALT  29143  bnj168  29195  bnj956  29245  bnj1098  29252  bnj1143  29259  bnj1146  29260  bnj1185  29263  bnj1196  29264  bnj600  29388  bnj849  29394  bnj906  29399  bnj916  29402  bnj983  29420  bnj984  29421  bnj1083  29445  bnj1176  29472  bnj1186  29474  bnj1189  29476  bnj1228  29478  bnj1253  29484  bnj1398  29501  bnj1463  29522  bnj1312  29525  bnj1514  29530  islshpat  29913  lsat0cv  29929  lshpsmreu  30005  atex  30301  islpln5  30430  islvol5  30474  pmapglb  30665  pmapglb2N  30666  pmapglb2xN  30667  elpaddn0  30695  pmapjat1  30748  polval2N  30801  osumcllem11N  30861  pexmidlem8N  30872  cdlemftr3  31460  dibelval3  32043  dibglbN  32062  dicelval3  32076  dihglbcpreN  32196  dihglb2  32238  dihjatcclem4  32317  mapdordlem2  32533  mapdrvallem2  32541  mapdpglem3  32571  hdmapglem7a  32826
  Copyright terms: Public domain W3C validator