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

Theorem rexlimdv 2933
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 2929 . 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 1804   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  rexlimdva  2935  rexlimdv3a  2937  rexlimdvw  2938  rexlimdvv  2941  elpwunsn  4055  trintss  4546  eldmrexrnb  6023  dffo3  6031  weniso  6235  ssorduni  6606  onint  6615  limuni3  6672  funcnvuni  6738  frxp  6895  smoiun  7034  tfrlem9  7056  oaordex  7209  oalimcl  7211  oaass  7212  omlimcl  7229  fisucdomOLD  7725  findcard3  7765  frfi  7767  unblem1  7774  ordiso2  7943  inf3lem3  8050  noinfepOLD  8080  r1sdom  8195  tz9.12lem3  8210  karden  8316  infxpenlem  8394  cardinfima  8481  iunfictbso  8498  dfac5  8512  cfflb  8642  cfcoflem  8655  cfcof  8657  fin23lem11  8700  fin23lem30  8725  fin1a2lem13  8795  axdc3lem2  8834  konigthlem  8946  alephval2  8950  pwcfsdom  8961  fpwwe2lem12  9022  tskuni  9164  axgroth6  9209  nqereu  9310  genpnmax  9388  ltaddpr  9415  recexsrlem  9483  mulgt0sr  9485  recexsr  9487  axrrecex  9543  axpre-sup  9549  addid1  9763  addid2  9766  recex  10188  zdiv  10940  btwnz  10973  lbzbi  11181  qbtwnre  11409  caubnd  13173  divalglem9  14041  unbenlem  14408  firest  14812  imasmnd2  15936  imasgrp2  16164  pmtrfrn  16462  pgpfi  16604  sylow2blem3  16621  imasring  17247  lspsneq  17747  lspdisj  17750  unitgOLD  19447  fctop  19483  cctop  19485  elcls  19552  elcls3  19562  subbascn  19733  cmpsublem  19877  cmpsub  19878  nllyidm  19968  comppfsc  20011  ptpjopn  20091  fbfinnfr  20320  filin  20333  isfil2  20335  infil  20342  fgss2  20353  fgfil  20354  fgcl  20357  fgabs  20358  elfm2  20427  rnelfm  20432  fmfnfmlem2  20434  fmfnfmlem4  20436  fmco  20440  flffbas  20474  cnpflf2  20479  fclscf  20504  alexsubALTlem2  20526  alexsubALTlem3  20527  alexsubALTlem4  20528  alexsubALT  20529  neibl  20982  met2ndc  21004  metcnp3  21021  icccmplem2  21306  xrge0tsms  21317  fgcfil  21688  volfiniun  21935  dyadmax  21985  dyadmbllem  21986  c1liplem1  22375  dgrlem  22604  axcontlem10  24254  usgrarnedg  24362  erclwwlksym  24792  erclwwlknsym  24804  lpni  25159  grpoidinvlem3  25186  grporcan  25201  grpoinvf  25220  nmosetre  25657  omlsii  26299  spansncol  26464  spansnss  26467  normcan  26472  spanunsni  26475  h1datomi  26477  nmopsetretALT  26760  nmfnsetre  26774  branmfn  27002  superpos  27251  chjatom  27254  cvbr4i  27264  atomli  27279  xrge0tsmsd  27753  eulerpartlemgh  28295  dfon2lem6  29196  trpredrec  29297  colineardim1  29687  finminlem  30112  nn0prpwlem  30116  neibastop2lem  30154  neibastop2  30155  fgmin  30164  heiborlem10  30292  prtlem15  30592  isnacs3  30618  jm2.26  30920  fnwe2lem2  30973  hbtlem5  31053  islptre  31579  limcperiod  31588  limclner  31611  coskpi2  31620  cosknegpi  31623  icccncfext  31644  stoweidlem27  31763  stoweidlem59  31795  fourierdlem41  31884  fourierdlem42  31885  fourierdlem70  31913  fourierdlem71  31914  fourierdlem81  31924  fourierswlem  31967  etransclem24  31995  etransclem32  32003  etransclem48  32019  islindeps2  32954  lshpcmp  34588  lsatn0  34599  lsatcmp  34603  lsmsat  34608  lsatcv0  34631  l1cvpat  34654  eqlkr  34699  lshpkrlem1  34710  lshpkrlem6  34715  lfl1dim  34721  lfl1dim2N  34722  lkrss2N  34769  athgt  35055  3dim2  35067  llnle  35117  llncmp  35121  lplnle  35139  lplnnle2at  35140  llncvrlpln2  35156  llncvrlpln  35157  lplncmp  35161  lplnexllnN  35163  lvolnle3at  35181  lplncvrlvol2  35214  lplncvrlvol  35215  lvolcmp  35216  pointpsubN  35350  pclfinN  35499  pclfinclN  35549  osumcllem11N  35565  pexmidlem4N  35572  cdleme17d3  36097  cdlemeg46gfre  36133  cdleme48gfv1  36137  cdleme50trn2  36152  trlord  36170  cdlemg6e  36223  cdlemj3  36424  diaelrnN  36647  diaintclN  36660  dia2dimlem6  36671  cdlemm10N  36720  dibintclN  36769  dihord6apre  36858  dihord5b  36861  dihord5apre  36864  dihglblem5apreN  36893  dihglblem2N  36896  dihglblem3N  36897  dihglbcpreN  36902  dihintcl  36946  lclkrlem2y  37133  lcfrvalsnN  37143
  Copyright terms: Public domain W3C validator