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

Theorem rexlimdv 2872
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Hypothesis
Ref Expression
rexlimdv.1  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimdv  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdv
StepHypRef Expression
1 rexlimdv.1 . . . 4  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
21com3l 81 . . 3  |-  ( x  e.  A  ->  ( ps  ->  ( ph  ->  ch ) ) )
32rexlimiv 2868 . 2  |-  ( E. x  e.  A  ps  ->  ( ph  ->  ch ) )
43com12 31 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-ral 2737  df-rex 2738
This theorem is referenced by:  rexlimdva  2874  rexlimdv3a  2876  rexlimdvw  2877  rexlimdvv  2880  elpwunsn  3985  trintss  4476  eldmrexrnb  5940  dffo3  5948  weniso  6151  ssorduni  6520  onint  6529  limuni3  6586  funcnvuni  6652  frxp  6809  smoiun  6950  tfrlem9  6972  oaordex  7125  oalimcl  7127  oaass  7128  omlimcl  7145  findcard3  7678  frfi  7680  unblem1  7687  ordiso2  7855  inf3lem3  7961  r1sdom  8105  tz9.12lem3  8120  karden  8226  infxpenlem  8304  cardinfima  8391  iunfictbso  8408  dfac5  8422  cfflb  8552  cfcoflem  8565  cfcof  8567  fin23lem11  8610  fin23lem30  8635  fin1a2lem13  8705  axdc3lem2  8744  konigthlem  8856  alephval2  8860  pwcfsdom  8871  fpwwe2lem12  8930  tskuni  9072  axgroth6  9117  nqereu  9218  genpnmax  9296  ltaddpr  9323  recexsrlem  9391  mulgt0sr  9393  recexsr  9395  axrrecex  9451  axpre-sup  9457  addid1  9671  addid2  9674  recex  10098  zdiv  10850  btwnz  10881  lbzbi  11089  qbtwnre  11319  caubnd  13193  divalglem9  14061  unbenlem  14428  firest  14840  imasmnd2  16074  imasgrp2  16302  pmtrfrn  16600  pgpfi  16742  sylow2blem3  16759  imasring  17381  lspsneq  17881  lspdisj  17884  unitgOLD  19554  fctop  19590  cctop  19592  elcls  19660  elcls3  19670  subbascn  19841  cmpsublem  19985  cmpsub  19986  nllyidm  20075  comppfsc  20118  ptpjopn  20198  fbfinnfr  20427  filin  20440  isfil2  20442  infil  20449  fgss2  20460  fgfil  20461  fgcl  20464  fgabs  20465  elfm2  20534  rnelfm  20539  fmfnfmlem2  20541  fmfnfmlem4  20543  fmco  20547  flffbas  20581  cnpflf2  20586  fclscf  20611  alexsubALTlem2  20633  alexsubALTlem3  20634  alexsubALTlem4  20635  alexsubALT  20636  neibl  21089  met2ndc  21111  metcnp3  21128  icccmplem2  21413  xrge0tsms  21424  fgcfil  21795  volfiniun  22042  dyadmax  22092  dyadmbllem  22093  c1liplem1  22482  dgrlem  22711  axcontlem10  24397  usgrarnedg  24505  erclwwlksym  24935  erclwwlknsym  24947  lpni  25302  grpoidinvlem3  25325  grporcan  25340  grpoinvf  25359  nmosetre  25796  omlsii  26438  spansncol  26603  spansnss  26606  normcan  26611  spanunsni  26614  h1datomi  26616  nmopsetretALT  26898  nmfnsetre  26912  branmfn  27140  superpos  27389  chjatom  27392  cvbr4i  27402  atomli  27417  xrge0tsmsd  27929  eulerpartlemgh  28500  dfon2lem6  29385  trpredrec  29486  colineardim1  29864  finminlem  30302  nn0prpwlem  30306  neibastop2lem  30344  neibastop2  30345  fgmin  30354  heiborlem10  30482  prtlem15  30782  isnacs3  30808  jm2.26  31110  fnwe2lem2  31163  hbtlem5  31245  islptre  31791  limcperiod  31800  limclner  31823  coskpi2  31832  cosknegpi  31835  icccncfext  31856  stoweidlem27  31975  stoweidlem59  32007  fourierdlem41  32096  fourierdlem42  32097  fourierdlem70  32125  fourierdlem71  32126  fourierdlem81  32136  fourierswlem  32179  islindeps2  33284  lshpcmp  35126  lsatn0  35137  lsatcmp  35141  lsmsat  35146  lsatcv0  35169  l1cvpat  35192  eqlkr  35237  lshpkrlem1  35248  lshpkrlem6  35253  lfl1dim  35259  lfl1dim2N  35260  lkrss2N  35307  athgt  35593  3dim2  35605  llnle  35655  llncmp  35659  lplnle  35677  lplnnle2at  35678  llncvrlpln2  35694  llncvrlpln  35695  lplncmp  35699  lplnexllnN  35701  lvolnle3at  35719  lplncvrlvol2  35752  lplncvrlvol  35753  lvolcmp  35754  pointpsubN  35888  pclfinN  36037  pclfinclN  36087  osumcllem11N  36103  pexmidlem4N  36110  cdleme17d3  36635  cdlemeg46gfre  36671  cdleme48gfv1  36675  cdleme50trn2  36690  trlord  36708  cdlemg6e  36761  cdlemj3  36962  diaelrnN  37185  diaintclN  37198  dia2dimlem6  37209  cdlemm10N  37258  dibintclN  37307  dihord6apre  37396  dihord5b  37399  dihord5apre  37402  dihglblem5apreN  37431  dihglblem2N  37434  dihglblem3N  37435  dihglbcpreN  37440  dihintcl  37484  lclkrlem2y  37671  lcfrvalsnN  37681
  Copyright terms: Public domain W3C validator