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

Definition df-rex 2676
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 2671 . 2  wff  E. x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1547 . 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  2680  rexnal  2681  rexbida  2685  rexbidv2  2693  rexbii2  2699  r2exf  2706  risset  2717  nfre1  2726  rexex  2729  rspe  2731  rsp2e  2733  reximi2  2776  reximdv2  2779  r19.23t  2784  r19.41  2824  reean  2838  rexeqf  2865  reu5  2885  rmo5  2888  cbvrexdva2  2901  rexv  2934  2gencl  2949  3gencl  2950  rspce  3011  ceqsrexv  3033  rexab  3061  rexab2  3065  rexrab2  3066  morex  3082  reu2  3086  reu6  3087  reu3  3088  2reuswap  3100  2reu5lem3  3105  2reu5  3106  rexun  3491  reuss2  3585  reuun2  3588  reupick  3589  reupick3  3590  reximdva0  3603  rabn0  3611  r19.2z  3681  r19.2zb  3682  rexsns  3809  exsnrex  3812  dfuni2  3981  eluni2  3983  elunirab  3992  iuncom4  4064  iunxiun  4137  intexrab  4323  reusv5OLD  4696  elxp2  4859  opeliunxp  4892  xpiundi  4895  xpiundir  4896  dmuni  5042  rnmpt  5079  elrnmpt1  5082  elres  5144  dfima2  5168  dfima3  5169  elima2  5172  dfco2a  5333  imaco  5338  dffo4  5848  dffo5  5849  zfrep6  5931  abrexco  5949  opabex3d  5952  opabex3  5953  abexssex  5965  abexex  5966  isomin  6020  frxp  6419  rdglim2  6653  oarec  6768  oeeu  6809  mapsn  7018  mapsnen  7147  pssnn  7290  unblem2  7323  dffi2  7390  marypha2lem4  7405  marypha2  7406  zfregcl  7522  axinf2  7555  zfinf2  7557  rankuni  7749  scott0  7770  cp  7775  bnd2  7777  infpwfien  7903  aceq1  7958  dfac5lem2  7965  dfac5lem3  7966  dfac2  7971  kmlem3  7992  kmlem6  7995  kmlem8  7997  kmlem14  8003  infmap2  8058  ackbij2  8083  cfub  8089  cfval2  8100  cflim3  8102  cfss  8105  cfslb  8106  isf32lem9  8201  zorn2lem6  8341  iundom2g  8375  winalim2  8531  grothprim  8669  genpass  8846  nqpr  8851  1idpr  8866  ltexprlem4  8876  ltexprlem5  8877  reclem2pr  8885  axrrecex  8998  sup2  9924  infm3  9927  nnunb  10177  2rexuz  10489  nnwos  10504  xrsupsslem  10845  xrinfmsslem  10846  maxprmfct  13072  vdwapun  13301  vdwmc  13305  vdwmc2  13306  ram0  13349  imasleval  13725  mreexexlem2d  13829  isssc  13979  drsdirfi  14354  dirge  14641  odcau  15197  ablfac2  15606  lspprat  16184  lidlnz  16258  isbasis2g  16972  tgval2  16980  ntreq0  17100  neitr  17202  cmpfi  17429  is1stc2  17462  2ndcsb  17469  2ndcsep  17479  1stcelcls  17481  hausmapdom  17520  isfbas2  17824  fbssint  17827  isfil2  17845  elfg  17860  fgcl  17867  uffix2  17913  alexsubALTlem4  18038  lpbl  18490  metustexhalfOLD  18550  metustexhalf  18551  metuel2  18566  restmetu  18574  bcthlem5  19238  umgraex  21315  usgraedg4  21363  uvtx01vtx  21458  3v3e3cycl2  21608  ubthlem1  22329  axhcompl-zf  22458  isch3  22701  shne0i  22907  cnlnssadj  23540  2reuswap2  23932  rexunirn  23935  rmoxfrdOLD  23936  rmoxfrd  23937  abrexdomjm  23945  abrexexd  23947  ishashinf  24116  erdszelem10  24843  ptpcon  24877  dedekind  25144  coep  25326  coepr  25327  dffr5  25328  dfpo2  25330  dfon2lem8  25364  tfrALTlem  25494  brimg  25694  dfrdg4  25707  tfrqfree  25708  ellines  25994  neifg  26294  abrexdom  26326  prdstotbnd  26397  n0el  26602  prtlem17  26619  prter2  26624  psgnunilem4  27292  rexbidar  27520  ssrexf  27555  rspcegf  27565  cncmpmax  27574  rfcnnnub  27578  stoweidlem14  27634  stoweidlem27  27647  stoweidlem34  27654  stoweidlem35  27655  stoweidlem43  27663  stoweidlem44  27664  stoweidlem50  27670  stoweidlem54  27674  stoweidlem56  27676  stoweidlem59  27679  stoweidlem60  27680  2rmoswap  27833  frisusgranb  28105  frgra3vlem2  28109  3vfriswmgralem  28112  frgrancvvdeqlemC  28146  usg2spot2nb  28172  onfrALTlem5  28343  onfrALTlem2  28347  onfrALTlem1  28349  onfrALTlem5VD  28710  onfrALTlem2VD  28714  onfrALTlem1VD  28715  chordthmALT  28759  bnj168  28807  bnj956  28857  bnj1098  28864  bnj1143  28871  bnj1146  28872  bnj1185  28875  bnj1196  28876  bnj600  29000  bnj849  29006  bnj906  29011  bnj916  29014  bnj983  29032  bnj984  29033  bnj1083  29057  bnj1176  29084  bnj1186  29086  bnj1189  29088  bnj1228  29090  bnj1253  29096  bnj1398  29113  bnj1463  29134  bnj1312  29137  bnj1514  29142  islshpat  29504  lsat0cv  29520  lshpsmreu  29596  atex  29892  islpln5  30021  islvol5  30065  pmapglb  30256  pmapglb2N  30257  pmapglb2xN  30258  elpaddn0  30286  pmapjat1  30339  polval2N  30392  osumcllem11N  30452  pexmidlem8N  30463  cdlemftr3  31051  dibelval3  31634  dibglbN  31653  dicelval3  31667  dihglbcpreN  31787  dihglb2  31829  dihjatcclem4  31908  mapdordlem2  32124  mapdrvallem2  32132  mapdpglem3  32162  hdmapglem7a  32417
  Copyright terms: Public domain W3C validator