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

Definition df-rex 2514
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 2510 . 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  2517  rexnal  2518  rexbida  2522  rexbidv2  2530  rexbii2  2536  r2exf  2541  risset  2552  nfre1  2561  rexex  2564  ra4e  2566  ra42e  2568  reximi2  2611  reximdv2  2614  r19.23t  2619  r19.41  2654  reean  2668  rexeqf  2687  rexv  2741  2gencl  2755  3gencl  2756  rcla4e  2816  ceqsrexv  2838  rexab  2865  rexab2  2869  rexrab2  2870  morex  2886  reurex  2890  reu5  2891  reu2  2892  reu6  2893  reu3  2894  2reuswap  2902  rexun  3263  reuss2  3355  reuun2  3358  reupick  3359  reupick3  3360  reximdva0  3373  rabn0  3381  r19.2z  3449  r19.2zb  3450  rexsns  3575  dfuni2  3729  eluni2  3731  elunirab  3740  iuncom4  3810  iunxiun  3882  intexrab  4068  reusv5OLD  4435  elxp2  4614  opeliunxp  4647  xpiundi  4650  xpiundir  4651  dmuni  4795  rnmpt  4832  elrnmpt1  4835  elres  4897  dfima2  4921  dfima3  4922  elima2  4925  dfco2a  5079  imaco  5084  dffo4  5528  dffo5  5529  zfrep6  5600  abrexco  5618  opabex3  5621  abexssex  5633  abexex  5634  isomin  5686  frxp  6077  rdglim2  6331  oarec  6446  oeeu  6487  mapsn  6695  mapsnen  6823  pssnn  6966  unblem2  6995  dffi2  7060  marypha2lem4  7075  marypha2  7076  zfregcl  7192  axinf2  7225  zfinf2  7227  rankuni  7419  scott0  7440  cp  7445  bnd2  7447  infpwfien  7573  aceq1  7628  dfac5lem2  7635  dfac5lem3  7636  dfac2  7641  kmlem3  7662  kmlem6  7665  kmlem8  7667  kmlem14  7673  infmap2  7728  ackbij2  7753  cfub  7759  cfval2  7770  cflim3  7772  cfss  7775  cfslb  7776  isf32lem9  7871  zorn2lem6  8012  iundom2g  8046  winalim2  8198  grothprim  8336  genpass  8513  nqpr  8518  1idpr  8533  ltexprlem4  8543  ltexprlem5  8544  reclem2pr  8552  axrrecex  8665  sup2  9590  infm3  9593  nnunb  9840  2rexuz  10150  nnwos  10165  xrsupsslem  10503  xrinfmsslem  10504  maxprmfct  12666  vdwapun  12895  vdwmc  12899  vdwmc2  12900  ram0  12943  imasleval  13317  isssc  13541  drsdirfi  13916  dirge  14194  odcau  14750  ablfac2  15159  lspprat  15740  lidlnz  15812  isbasis2g  16518  tgval2  16526  ntreq0  16646  cmpfi  16967  is1stc2  17000  2ndcsb  17007  2ndcsep  17017  1stcelcls  17019  hausmapdom  17058  isfbas2  17362  fbssint  17365  isfil2  17383  elfg  17398  fgcl  17405  uffix2  17451  alexsubALTlem4  17576  lpbl  17881  bcthlem5  18582  ubthlem1  21279  axhcompl-zf  21408  isch3  21651  shne0i  21857  cnlnssadj  22490  erdszelem10  22902  ptpcon  22935  umgraex  23046  dedekind  23252  coep  23278  coepr  23279  dffr5  23280  dfpo2  23282  dfon2lem8  23314  tfrALTlem  23444  axfelem18  23531  brimg  23650  dfrdg4  23662  tfrqfree  23663  ellines  23949  fates  24120  dstr  24337  domncnt  24448  ranncnt  24449  dfdir2  24457  apnei  24686  gltpntl2  25239  isconcl7a  25271  bosser  25333  neifg  25486  abrexdom  25571  prdstotbnd  25684  n0el  25891  prtlem17  25910  prter2  25915  psgnunilem4  26586  rexbidar  26816  ssrexf  26851  rcla4egf  26861  cncmpmax  26870  rfcnnnub  26874  stoweidlem14  26897  stoweidlem27  26910  stoweidlem34  26917  stoweidlem35  26918  stoweidlem43  26926  stoweidlem44  26927  stoweidlem50  26933  stoweidlem54  26937  stoweidlem56  26939  stoweidlem57  26940  stoweidlem59  26942  stoweidlem60  26943  onfrALTlem5  27097  onfrALTlem2  27101  onfrALTlem1  27103  onfrALTlem5VD  27448  onfrALTlem2VD  27452  onfrALTlem1VD  27453  bnj168  27544  bnj956  27594  bnj1098  27601  bnj1143  27608  bnj1146  27609  bnj1185  27612  bnj1196  27613  bnj600  27737  bnj849  27743  bnj906  27748  bnj916  27751  bnj983  27769  bnj984  27770  bnj1083  27794  bnj1176  27821  bnj1186  27823  bnj1189  27825  bnj1228  27827  bnj1253  27833  bnj1398  27850  bnj1463  27871  bnj1312  27874  bnj1514  27879  islshpat  28111  lsat0cv  28127  lshpsmreu  28203  atex  28499  islpln5  28628  islvol5  28672  pmapglb  28863  pmapglb2N  28864  pmapglb2xN  28865  elpaddn0  28893  pmapjat1  28946  polval2N  28999  osumcllem11N  29059  pexmidlem8N  29070  cdlemftr3  29658  dibelval3  30241  dibglbN  30260  dicelval3  30274  dihglbcpreN  30394  dihglb2  30436  dihjatcclem4  30515  mapdordlem2  30731  mapdrvallem2  30739  mapdpglem3  30769  hdmapglem7a  31024
  Copyright terms: Public domain W3C validator