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

Definition df-rex 2552
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 2547 . 2  wff  E. x  e.  A  ph
52cv 1624 . . . . 5  class  x
65, 3wcel 1687 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1530 . 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  2556  rexnal  2557  rexbida  2561  rexbidv2  2569  rexbii2  2575  r2exf  2582  risset  2593  nfre1  2602  rexex  2605  rspe  2607  rsp2e  2609  reximi2  2652  reximdv2  2655  r19.23t  2660  r19.41  2695  reean  2709  rexeqf  2736  reu5  2756  rmo5  2759  cbvrexdva2  2772  rexv  2805  2gencl  2820  3gencl  2821  rspce  2882  ceqsrexv  2904  rexab  2931  rexab2  2935  rexrab2  2936  morex  2952  reu2  2956  reu6  2957  reu3  2958  2reuswap  2970  2reu5lem3  2975  2reu5  2976  rexun  3358  reuss2  3451  reuun2  3454  reupick  3455  reupick3  3456  reximdva0  3469  rabn0  3477  r19.2z  3546  r19.2zb  3547  rexsns  3674  dfuni2  3832  eluni2  3834  elunirab  3843  iuncom4  3915  iunxiun  3987  intexrab  4175  reusv5OLD  4545  elxp2  4708  opeliunxp  4741  xpiundi  4744  xpiundir  4745  dmuni  4889  rnmpt  4926  elrnmpt1  4929  elres  4991  dfima2  5015  dfima3  5016  elima2  5019  dfco2a  5173  imaco  5178  dffo4  5639  dffo5  5640  zfrep6  5711  abrexco  5729  opabex3  5732  abexssex  5744  abexex  5745  isomin  5797  frxp  6188  rdglim2  6442  oarec  6557  oeeu  6598  mapsn  6806  mapsnen  6935  pssnn  7078  unblem2  7107  dffi2  7173  marypha2lem4  7188  marypha2  7189  zfregcl  7305  axinf2  7338  zfinf2  7340  rankuni  7532  scott0  7553  cp  7558  bnd2  7560  infpwfien  7686  aceq1  7741  dfac5lem2  7748  dfac5lem3  7749  dfac2  7754  kmlem3  7775  kmlem6  7778  kmlem8  7780  kmlem14  7786  infmap2  7841  ackbij2  7866  cfub  7872  cfval2  7883  cflim3  7885  cfss  7888  cfslb  7889  isf32lem9  7984  zorn2lem6  8125  iundom2g  8159  winalim2  8315  grothprim  8453  genpass  8630  nqpr  8635  1idpr  8650  ltexprlem4  8660  ltexprlem5  8661  reclem2pr  8669  axrrecex  8782  sup2  9707  infm3  9710  nnunb  9958  2rexuz  10268  nnwos  10283  xrsupsslem  10621  xrinfmsslem  10622  maxprmfct  12788  vdwapun  13017  vdwmc  13021  vdwmc2  13022  ram0  13065  imasleval  13439  mreexexlem2d  13543  isssc  13693  drsdirfi  14068  dirge  14355  odcau  14911  ablfac2  15320  lspprat  15902  lidlnz  15976  isbasis2g  16682  tgval2  16690  ntreq0  16810  cmpfi  17131  is1stc2  17164  2ndcsb  17171  2ndcsep  17181  1stcelcls  17183  hausmapdom  17222  isfbas2  17526  fbssint  17529  isfil2  17547  elfg  17562  fgcl  17569  uffix2  17615  alexsubALTlem4  17740  lpbl  18045  bcthlem5  18746  ubthlem1  21443  axhcompl-zf  21572  isch3  21815  shne0i  22021  cnlnssadj  22654  erdszelem10  23137  ptpcon  23170  umgraex  23281  dedekind  23487  coep  23513  coepr  23514  dffr5  23515  dfpo2  23517  dfon2lem8  23549  tfrALTlem  23679  axfelem18  23766  brimg  23885  dfrdg4  23897  tfrqfree  23898  ellines  24184  fates  24355  dstr  24572  domncnt  24683  ranncnt  24684  dfdir2  24692  apnei  24921  gltpntl2  25474  isconcl7a  25506  bosser  25568  neifg  25721  abrexdom  25806  prdstotbnd  25919  n0el  26126  prtlem17  26145  prter2  26150  psgnunilem4  26821  rexbidar  27050  ssrexf  27085  rspcegf  27095  cncmpmax  27104  rfcnnnub  27108  stoweidlem14  27164  stoweidlem27  27177  stoweidlem34  27184  stoweidlem35  27185  stoweidlem43  27193  stoweidlem44  27194  stoweidlem50  27200  stoweidlem54  27204  stoweidlem56  27206  stoweidlem57  27207  stoweidlem59  27209  stoweidlem60  27210  2rmoswap  27343  onfrALTlem5  27580  onfrALTlem2  27584  onfrALTlem1  27586  onfrALTlem5VD  27931  onfrALTlem2VD  27935  onfrALTlem1VD  27936  bnj168  28027  bnj956  28077  bnj1098  28084  bnj1143  28091  bnj1146  28092  bnj1185  28095  bnj1196  28096  bnj600  28220  bnj849  28226  bnj906  28231  bnj916  28234  bnj983  28252  bnj984  28253  bnj1083  28277  bnj1176  28304  bnj1186  28306  bnj1189  28308  bnj1228  28310  bnj1253  28316  bnj1398  28333  bnj1463  28354  bnj1312  28357  bnj1514  28362  islshpat  28476  lsat0cv  28492  lshpsmreu  28568  atex  28864  islpln5  28993  islvol5  29037  pmapglb  29228  pmapglb2N  29229  pmapglb2xN  29230  elpaddn0  29258  pmapjat1  29311  polval2N  29364  osumcllem11N  29424  pexmidlem8N  29435  cdlemftr3  30023  dibelval3  30606  dibglbN  30625  dicelval3  30639  dihglbcpreN  30759  dihglb2  30801  dihjatcclem4  30880  mapdordlem2  31096  mapdrvallem2  31104  mapdpglem3  31134  hdmapglem7a  31389
  Copyright terms: Public domain W3C validator