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

Definition df-rex 2799
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  setvar  x
3 cA . . 3  class  A
41, 2, 3wrex 2794 . 2  wff  E. x  e.  A  ph
52cv 1382 . . . . 5  class  x
65, 3wcel 1804 . . . 4  wff  x  e.  A
76, 1wa 369 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1599 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 184 1  wff  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2889  rexnalOLD  2892  rexex  2900  rspe  2901  rsp2eOLD  2903  nfre1  2904  reximi2  2910  reximd2a  2913  reximdv2  2914  r19.23t  2921  rexbii2  2943  rexbida  2949  rexbidv2  2950  r2exfOLD  2965  risset  2968  r19.41v  2995  r19.41  2996  reean  3010  rexeqf  3037  reu5  3059  rmo5  3062  cbvrexdva2  3075  rexv  3110  2gencl  3126  3gencl  3127  rspce  3191  ceqsrexv  3219  rexab  3248  rexab2  3252  rexrab2  3253  morex  3269  reu2  3273  reu6  3274  reu3  3275  2reuswap  3288  2reu5lem3  3293  2reu5  3294  rexun  3669  reuss2  3763  reuun2  3766  reupick  3767  reupick3  3768  reximdva0  3782  rabn0  3791  r19.2z  3904  r19.2zb  3905  rexsns  4047  rexsnsOLD  4048  exsnrex  4052  dfuni2  4236  eluni2  4238  elunirab  4246  iuncom4  4323  iunxiun  4398  intexrab  4596  reusv5OLD  4647  elxp2  5007  opeliunxp  5041  xpiundi  5044  xpiundir  5045  dmuni  5202  rnmpt  5238  elrnmpt1  5241  elres  5299  dfima2  5329  dfima3  5330  elima2  5333  dfco2a  5497  imaco  5502  dffo4  6032  dffo5  6033  abrexco  6141  isomin  6218  zfrep6  6753  opabex3d  6763  opabex3  6764  abexssex  6767  abexex  6768  frxp  6895  rdglim2  7100  oarec  7213  oeeu  7254  mapsn  7462  mapsnen  7595  pssnn  7740  unblem2  7775  dffi2  7885  marypha2lem4  7900  marypha2  7901  zfregcl  8023  axinf2  8060  zfinf2  8062  rankuni  8284  scott0  8307  cp  8312  bnd2  8314  infpwfien  8446  aceq1  8501  dfac5lem2  8508  dfac5lem3  8509  dfac2  8514  kmlem3  8535  kmlem6  8538  kmlem8  8540  kmlem14  8546  infmap2  8601  ackbij2  8626  cfub  8632  cfval2  8643  cflim3  8645  cfss  8648  cfslb  8649  isf32lem9  8744  zorn2lem6  8884  iundom2g  8918  winalim2  9077  grothprim  9215  genpass  9390  nqpr  9395  1idpr  9410  ltexprlem4  9420  ltexprlem5  9421  reclem2pr  9429  axrrecex  9543  dedekind  9747  sup2  10506  infm3  10509  nnunb  10798  2rexuz  11144  nnwos  11160  xrsupsslem  11509  xrinfmsslem  11510  cshwsexa  12774  wwlktovfo  12878  maxprmfct  14236  vdwapun  14474  vdwmc  14478  vdwmc2  14479  ram0  14522  imasleval  14920  mreexexlem2d  15024  isssc  15171  drsdirfi  15546  dirge  15846  psgnunilem4  16501  odcau  16603  ablfac2  17119  lspprat  17778  lidlnz  17855  isbasis2g  19427  tgval2  19435  ntreq0  19556  neitr  19659  cmpfi  19886  is1stc2  19921  2ndcsb  19928  2ndcsep  19938  1stcelcls  19940  hausmapdom  19979  isfbas2  20314  fbssint  20317  isfil2  20335  elfg  20350  fgcl  20357  uffix2  20403  alexsubALTlem4  20528  lpbl  20984  metustexhalfOLD  21044  metustexhalf  21045  metuel2  21060  restmetu  21068  bcthlem5  21745  umgraex  24301  usgraedg4  24365  uvtx01vtx  24470  3v3e3cycl2  24642  wlknwwlknsur  24690  wlkiswwlksur  24697  wwlkextsur  24709  frisusgranb  24975  frgra3vlem2  24979  3vfriswmgralem  24982  frgrancvvdeqlemC  25017  usg2spot2nb  25043  ubthlem1  25764  axhcompl-zf  25893  isch3  26137  shne0i  26344  cnlnssadj  26977  2reuswap2  27365  rexunirn  27368  rmoxfrdOLD  27369  rmoxfrd  27370  abrexdomjm  27383  abrexexd  27385  fpwrelmapffslem  27533  ishashinf  27584  ordtconlem1  27884  ddemeas  28186  eulerpartlemgvv  28293  erdszelem10  28622  ptpcon  28656  coep  29156  coepr  29157  dffr5  29158  dfpo2  29160  opelco3  29184  dfon2lem8  29198  brimg  29563  dfrdg4  29576  tfrqfree  29577  ellines  29778  neifg  30165  abrexdom  30197  prdstotbnd  30266  n0el  30576  prtlem17  30593  prter2  30598  rexbidar  31309  ssrexf  31342  rspcegf  31352  cncmpmax  31361  rfcnnnub  31365  suprnmpt  31405  ssfiunibd  31463  islpcn  31599  lptre2pt  31600  stoweidlem14  31750  stoweidlem34  31770  stoweidlem35  31771  stoweidlem43  31779  stoweidlem44  31780  stoweidlem50  31786  stoweidlem54  31790  stoweidlem56  31792  stoweidlem59  31795  stoweidlem60  31796  fourier2  31964  2rmoswap  32143  opeliun2xp  32790  onfrALTlem5  33182  onfrALTlem2  33186  onfrALTlem1  33188  onfrALTlem5VD  33553  onfrALTlem2VD  33557  onfrALTlem1VD  33558  chordthmALT  33601  bnj168  33653  bnj956  33703  bnj1098  33710  bnj1143  33717  bnj1146  33718  bnj1185  33720  bnj1196  33721  bnj600  33845  bnj849  33851  bnj906  33856  bnj916  33859  bnj983  33877  bnj984  33878  bnj1083  33902  bnj1176  33929  bnj1186  33931  bnj1189  33933  bnj1228  33935  bnj1253  33941  bnj1398  33958  bnj1463  33979  bnj1312  33982  bnj1514  33987  bj-rexvwv  34325  bj-rexcom4  34328  bj-snglc  34410  bj-snglss  34411  bj-finsumval0  34538  islshpat  34617  lsat0cv  34633  lshpsmreu  34709  atex  35005  islpln5  35134  islvol5  35178  pmapglb  35369  pmapglb2N  35370  pmapglb2xN  35371  elpaddn0  35399  pmapjat1  35452  polval2N  35505  osumcllem11N  35565  pexmidlem8N  35576  cdlemftr3  36166  dibelval3  36749  dibglbN  36768  dicelval3  36782  dihglbcpreN  36902  dihglb2  36944  dihjatcclem4  37023  mapdordlem2  37239  mapdrvallem2  37247  mapdpglem3  37277  hdmapglem7a  37532  rp-isfinite5  37581  rp-isfinite6  37582
  Copyright terms: Public domain W3C validator