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

Definition df-rex 2549
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 2544 . 2  wff  E. x  e.  A  ph
52cv 1622 . . . . 5  class  x
65, 3wcel 1684 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1528 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 176 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  2553  rexnal  2554  rexbida  2558  rexbidv2  2566  rexbii2  2572  r2exf  2579  risset  2590  nfre1  2599  rexex  2602  rspe  2604  rsp2e  2606  reximi2  2649  reximdv2  2652  r19.23t  2657  r19.41  2692  reean  2706  rexeqf  2733  reu5  2753  rmo5  2756  cbvrexdva2  2769  rexv  2802  2gencl  2817  3gencl  2818  rspce  2879  ceqsrexv  2901  rexab  2928  rexab2  2932  rexrab2  2933  morex  2949  reu2  2953  reu6  2954  reu3  2955  2reuswap  2967  2reu5lem3  2972  2reu5  2973  rexun  3355  reuss2  3448  reuun2  3451  reupick  3452  reupick3  3453  reximdva0  3466  rabn0  3474  r19.2z  3543  r19.2zb  3544  rexsns  3671  dfuni2  3829  eluni2  3831  elunirab  3840  iuncom4  3912  iunxiun  3984  intexrab  4170  reusv5OLD  4544  elxp2  4707  opeliunxp  4740  xpiundi  4743  xpiundir  4744  dmuni  4888  rnmpt  4925  elrnmpt1  4928  elres  4990  dfima2  5014  dfima3  5015  elima2  5018  dfco2a  5173  imaco  5178  dffo4  5676  dffo5  5677  zfrep6  5748  abrexco  5766  opabex3  5769  abexssex  5781  abexex  5782  isomin  5834  frxp  6225  rdglim2  6445  oarec  6560  oeeu  6601  mapsn  6809  mapsnen  6938  pssnn  7081  unblem2  7110  dffi2  7176  marypha2lem4  7191  marypha2  7192  zfregcl  7308  axinf2  7341  zfinf2  7343  rankuni  7535  scott0  7556  cp  7561  bnd2  7563  infpwfien  7689  aceq1  7744  dfac5lem2  7751  dfac5lem3  7752  dfac2  7757  kmlem3  7778  kmlem6  7781  kmlem8  7783  kmlem14  7789  infmap2  7844  ackbij2  7869  cfub  7875  cfval2  7886  cflim3  7888  cfss  7891  cfslb  7892  isf32lem9  7987  zorn2lem6  8128  iundom2g  8162  winalim2  8318  grothprim  8456  genpass  8633  nqpr  8638  1idpr  8653  ltexprlem4  8663  ltexprlem5  8664  reclem2pr  8672  axrrecex  8785  sup2  9710  infm3  9713  nnunb  9961  2rexuz  10271  nnwos  10286  xrsupsslem  10625  xrinfmsslem  10626  maxprmfct  12792  vdwapun  13021  vdwmc  13025  vdwmc2  13026  ram0  13069  imasleval  13443  mreexexlem2d  13547  isssc  13697  drsdirfi  14072  dirge  14359  odcau  14915  ablfac2  15324  lspprat  15906  lidlnz  15980  isbasis2g  16686  tgval2  16694  ntreq0  16814  cmpfi  17135  is1stc2  17168  2ndcsb  17175  2ndcsep  17185  1stcelcls  17187  hausmapdom  17226  isfbas2  17530  fbssint  17533  isfil2  17551  elfg  17566  fgcl  17573  uffix2  17619  alexsubALTlem4  17744  lpbl  18049  bcthlem5  18750  ubthlem1  21449  axhcompl-zf  21578  isch3  21821  shne0i  22027  cnlnssadj  22660  2reuswap2  23137  rexunirn  23140  rmoxfrdOLD  23146  rmoxfrd  23147  abrexdomjm  23165  abrexexd  23192  ishashinf  23389  erdszelem10  23731  ptpcon  23764  umgraex  23875  dedekind  24082  coep  24108  coepr  24109  dffr5  24110  dfpo2  24112  dfon2lem8  24146  tfrALTlem  24276  brimg  24476  dfrdg4  24488  tfrqfree  24489  ellines  24775  fates  24955  dstr  25171  domncnt  25282  ranncnt  25283  dfdir2  25291  apnei  25520  gltpntl2  26073  isconcl7a  26105  bosser  26167  neifg  26320  abrexdom  26405  prdstotbnd  26518  n0el  26725  prtlem17  26744  prter2  26749  psgnunilem4  27420  rexbidar  27649  ssrexf  27684  rspcegf  27694  cncmpmax  27703  rfcnnnub  27707  stoweidlem14  27763  stoweidlem27  27776  stoweidlem34  27783  stoweidlem35  27784  stoweidlem43  27792  stoweidlem44  27793  stoweidlem50  27799  stoweidlem54  27803  stoweidlem56  27805  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  2rmoswap  27962  uvtx01vtx  28164  frgra3vlem2  28179  3vfriswmgralem  28182  onfrALTlem5  28307  onfrALTlem2  28311  onfrALTlem1  28313  onfrALTlem5VD  28661  onfrALTlem2VD  28665  onfrALTlem1VD  28666  chordthmALT  28710  bnj168  28758  bnj956  28808  bnj1098  28815  bnj1143  28822  bnj1146  28823  bnj1185  28826  bnj1196  28827  bnj600  28951  bnj849  28957  bnj906  28962  bnj916  28965  bnj983  28983  bnj984  28984  bnj1083  29008  bnj1176  29035  bnj1186  29037  bnj1189  29039  bnj1228  29041  bnj1253  29047  bnj1398  29064  bnj1463  29085  bnj1312  29088  bnj1514  29093  islshpat  29207  lsat0cv  29223  lshpsmreu  29299  atex  29595  islpln5  29724  islvol5  29768  pmapglb  29959  pmapglb2N  29960  pmapglb2xN  29961  elpaddn0  29989  pmapjat1  30042  polval2N  30095  osumcllem11N  30155  pexmidlem8N  30166  cdlemftr3  30754  dibelval3  31337  dibglbN  31356  dicelval3  31370  dihglbcpreN  31490  dihglb2  31532  dihjatcclem4  31611  mapdordlem2  31827  mapdrvallem2  31835  mapdpglem3  31865  hdmapglem7a  32120
  Copyright terms: Public domain W3C validator