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

Theorem rexlimdv 2953
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 2949 . 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 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimdva  2955  rexlimdv3a  2957  rexlimdvw  2958  rexlimdvv  2961  elpwunsn  4068  trintss  4556  eldmrexrnb  6026  dffo3  6034  weniso  6236  ssorduni  6599  onint  6608  limuni3  6665  funcnvuni  6734  frxp  6890  smoiun  7029  tfrlem9  7051  oaordex  7204  oalimcl  7206  oaass  7207  omlimcl  7224  fisucdomOLD  7720  findcard3  7759  frfi  7761  unblem1  7768  ordiso2  7936  inf3lem3  8043  noinfepOLD  8073  r1sdom  8188  tz9.12lem3  8203  karden  8309  infxpenlem  8387  cardinfima  8474  iunfictbso  8491  dfac5  8505  cfflb  8635  cfcoflem  8648  cfcof  8650  fin23lem11  8693  fin23lem30  8718  fin1a2lem13  8788  axdc3lem2  8827  konigthlem  8939  alephval2  8943  pwcfsdom  8954  fpwwe2lem12  9015  tskuni  9157  axgroth6  9202  nqereu  9303  genpnmax  9381  ltaddpr  9408  recexsrlem  9476  mulgt0sr  9478  recexsr  9480  axrrecex  9536  axpre-sup  9542  addid1  9755  addid2  9758  recex  10177  zdiv  10927  btwnz  10959  lbzbi  11166  qbtwnre  11394  caubnd  13147  divalglem9  13911  unbenlem  14278  firest  14681  imasmnd2  15768  imasgrp2  15982  pmtrfrn  16276  pgpfi  16418  sylow2blem3  16435  imasrng  17049  lspsneq  17548  lspdisj  17551  unitg  19232  fctop  19268  cctop  19270  elcls  19337  elcls3  19347  subbascn  19518  cmpsublem  19662  cmpsub  19663  nllyidm  19753  ptpjopn  19845  fbfinnfr  20074  filin  20087  isfil2  20089  infil  20096  fgss2  20107  fgfil  20108  fgcl  20111  fgabs  20112  elfm2  20181  rnelfm  20186  fmfnfmlem2  20188  fmfnfmlem4  20190  fmco  20194  flffbas  20228  cnpflf2  20233  fclscf  20258  alexsubALTlem2  20280  alexsubALTlem3  20281  alexsubALTlem4  20282  alexsubALT  20283  neibl  20736  met2ndc  20758  metcnp3  20775  icccmplem2  21060  xrge0tsms  21071  fgcfil  21442  volfiniun  21689  dyadmax  21739  dyadmbllem  21740  c1liplem1  22129  dgrlem  22358  axcontlem10  23949  usgrarnedg  24057  erclwwlksym  24487  erclwwlknsym  24499  lpni  24854  grpoidinvlem3  24881  grpoidinvlem4  24882  grporcan  24896  grpoinvf  24915  nmosetre  25352  omlsii  25994  spansncol  26159  spansnss  26162  normcan  26167  spanunsni  26170  h1datomi  26172  nmopsetretALT  26455  nmfnsetre  26469  branmfn  26697  cnvbraval  26702  opsqrlem1  26732  superpos  26946  chjatom  26949  cvbr4i  26959  atomli  26974  xrge0tsmsd  27435  eulerpartlemgh  27954  dfon2lem6  28794  trpredrec  28895  colineardim1  29285  finminlem  29711  nn0prpwlem  29715  comppfsc  29777  neibastop2lem  29779  neibastop2  29780  fgmin  29789  heiborlem10  29917  prtlem15  30218  isnacs3  30244  jm2.26  30548  fnwe2lem2  30601  lnrfg  30672  hbtlem5  30681  climsuse  31150  islptre  31161  limccog  31162  limcperiod  31170  0ellimcdiv  31191  limclner  31193  coskpi2  31202  cosknegpi  31205  cncfshift  31212  cncfperiod  31217  cncfuni  31225  icccncfext  31226  itgperiod  31299  stoweidlem27  31327  stoweidlem59  31359  fourierdlem41  31448  fourierdlem42  31449  fourierdlem48  31455  fourierdlem49  31456  fourierdlem52  31459  fourierdlem54  31461  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem77  31484  fourierdlem81  31488  fourierdlem83  31490  fourierdlem87  31494  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem113  31520  fourierdlem114  31521  fourierswlem  31531  islindeps2  32157  lshpcmp  33785  lsatn0  33796  lsatcmp  33800  lsmsat  33805  lsatcv0  33828  l1cvpat  33851  eqlkr  33896  lshpkrlem1  33907  lshpkrlem6  33912  lfl1dim  33918  lfl1dim2N  33919  lkrss2N  33966  athgt  34252  3dim2  34264  llnle  34314  llncmp  34318  lplnle  34336  lplnnle2at  34337  llncvrlpln2  34353  llncvrlpln  34354  lplncmp  34358  lplnexllnN  34360  lvolnle3at  34378  lplncvrlvol2  34411  lplncvrlvol  34412  lvolcmp  34413  pointpsubN  34547  pclfinN  34696  pclfinclN  34746  osumcllem11N  34762  pexmidlem4N  34769  lhprelat3N  34836  cdleme17d3  35292  cdlemeg46gfre  35328  cdleme48gfv1  35332  cdleme50trn2  35347  trlord  35365  cdlemg6e  35418  cdlemj3  35619  diaelrnN  35842  diaintclN  35855  dia2dimlem6  35866  cdlemm10N  35915  dibintclN  35964  dihord6apre  36053  dihord5b  36056  dihord5apre  36059  dihglblem5apreN  36088  dihglblem2N  36091  dihglblem3N  36092  dihglbcpreN  36097  dihintcl  36141  lclkrlem2y  36328  lcfrvalsnN  36338
  Copyright terms: Public domain W3C validator