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

Definition df-rex 2522
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 2517 . 2  wff  E. x  e.  A  ph
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1537 . 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  2526  rexnal  2527  rexbida  2531  rexbidv2  2539  rexbii2  2545  r2exf  2552  risset  2563  nfre1  2572  rexex  2575  ra4e  2577  ra42e  2579  reximi2  2622  reximdv2  2625  r19.23t  2630  r19.41  2665  reean  2679  rexeqf  2706  reu5  2723  rmo5  2726  cbvrexdva2  2738  rexv  2771  2gencl  2785  3gencl  2786  rcla4e  2847  ceqsrexv  2869  rexab  2896  rexab2  2900  rexrab2  2901  morex  2917  reu2  2921  reu6  2922  reu3  2923  2reuswap  2933  rexun  3316  reuss2  3409  reuun2  3412  reupick  3413  reupick3  3414  reximdva0  3427  rabn0  3435  r19.2z  3504  r19.2zb  3505  rexsns  3631  dfuni2  3789  eluni2  3791  elunirab  3800  iuncom4  3872  iunxiun  3944  intexrab  4132  reusv5OLD  4502  elxp2  4681  opeliunxp  4714  xpiundi  4717  xpiundir  4718  dmuni  4862  rnmpt  4899  elrnmpt1  4902  elres  4964  dfima2  4988  dfima3  4989  elima2  4992  dfco2a  5146  imaco  5151  dffo4  5596  dffo5  5597  zfrep6  5668  abrexco  5686  opabex3  5689  abexssex  5701  abexex  5702  isomin  5754  frxp  6145  rdglim2  6399  oarec  6514  oeeu  6555  mapsn  6763  mapsnen  6892  pssnn  7035  unblem2  7064  dffi2  7130  marypha2lem4  7145  marypha2  7146  zfregcl  7262  axinf2  7295  zfinf2  7297  rankuni  7489  scott0  7510  cp  7515  bnd2  7517  infpwfien  7643  aceq1  7698  dfac5lem2  7705  dfac5lem3  7706  dfac2  7711  kmlem3  7732  kmlem6  7735  kmlem8  7737  kmlem14  7743  infmap2  7798  ackbij2  7823  cfub  7829  cfval2  7840  cflim3  7842  cfss  7845  cfslb  7846  isf32lem9  7941  zorn2lem6  8082  iundom2g  8116  winalim2  8272  grothprim  8410  genpass  8587  nqpr  8592  1idpr  8607  ltexprlem4  8617  ltexprlem5  8618  reclem2pr  8626  axrrecex  8739  sup2  9664  infm3  9667  nnunb  9914  2rexuz  10224  nnwos  10239  xrsupsslem  10577  xrinfmsslem  10578  maxprmfct  12740  vdwapun  12969  vdwmc  12973  vdwmc2  12974  ram0  13017  imasleval  13391  mreexexlem2d  13495  isssc  13645  drsdirfi  14020  dirge  14307  odcau  14863  ablfac2  15272  lspprat  15854  lidlnz  15928  isbasis2g  16634  tgval2  16642  ntreq0  16762  cmpfi  17083  is1stc2  17116  2ndcsb  17123  2ndcsep  17133  1stcelcls  17135  hausmapdom  17174  isfbas2  17478  fbssint  17481  isfil2  17499  elfg  17514  fgcl  17521  uffix2  17567  alexsubALTlem4  17692  lpbl  17997  bcthlem5  18698  ubthlem1  21395  axhcompl-zf  21524  isch3  21767  shne0i  21973  cnlnssadj  22606  erdszelem10  23089  ptpcon  23122  umgraex  23233  dedekind  23439  coep  23465  coepr  23466  dffr5  23467  dfpo2  23469  dfon2lem8  23501  tfrALTlem  23631  axfelem18  23718  brimg  23837  dfrdg4  23849  tfrqfree  23850  ellines  24136  fates  24307  dstr  24524  domncnt  24635  ranncnt  24636  dfdir2  24644  apnei  24873  gltpntl2  25426  isconcl7a  25458  bosser  25520  neifg  25673  abrexdom  25758  prdstotbnd  25871  n0el  26078  prtlem17  26097  prter2  26102  psgnunilem4  26773  rexbidar  27003  ssrexf  27038  rcla4egf  27048  cncmpmax  27057  rfcnnnub  27061  stoweidlem14  27084  stoweidlem27  27097  stoweidlem34  27104  stoweidlem35  27105  stoweidlem43  27113  stoweidlem44  27114  stoweidlem50  27120  stoweidlem54  27124  stoweidlem56  27126  stoweidlem57  27127  stoweidlem59  27129  stoweidlem60  27130  onfrALTlem5  27344  onfrALTlem2  27348  onfrALTlem1  27350  onfrALTlem5VD  27695  onfrALTlem2VD  27699  onfrALTlem1VD  27700  bnj168  27791  bnj956  27841  bnj1098  27848  bnj1143  27855  bnj1146  27856  bnj1185  27859  bnj1196  27860  bnj600  27984  bnj849  27990  bnj906  27995  bnj916  27998  bnj983  28016  bnj984  28017  bnj1083  28041  bnj1176  28068  bnj1186  28070  bnj1189  28072  bnj1228  28074  bnj1253  28080  bnj1398  28097  bnj1463  28118  bnj1312  28121  bnj1514  28126  islshpat  28358  lsat0cv  28374  lshpsmreu  28450  atex  28746  islpln5  28875  islvol5  28919  pmapglb  29110  pmapglb2N  29111  pmapglb2xN  29112  elpaddn0  29140  pmapjat1  29193  polval2N  29246  osumcllem11N  29306  pexmidlem8N  29317  cdlemftr3  29905  dibelval3  30488  dibglbN  30507  dicelval3  30521  dihglbcpreN  30641  dihglb2  30683  dihjatcclem4  30762  mapdordlem2  30978  mapdrvallem2  30986  mapdpglem3  31016  hdmapglem7a  31271
  Copyright terms: Public domain W3C validator