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

Theorem rexlimdv 2912
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 84 . . 3  |-  ( x  e.  A  ->  ( ps  ->  ( ph  ->  ch ) ) )
32rexlimiv 2908 . 2  |-  ( E. x  e.  A  ps  ->  ( ph  ->  ch ) )
43com12 32 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   E.wrex 2772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2776  df-rex 2777
This theorem is referenced by:  rexlimdva  2914  rexlimdv3a  2916  rexlimdvw  2917  rexlimdvv  2920  elpwunsn  4040  trintss  4534  eldmrexrnb  6044  dffo3  6052  weniso  6260  ssorduni  6626  onint  6636  limuni3  6693  funcnvuni  6760  frxp  6917  smoiun  7091  tfrlem9  7114  oaordex  7270  oalimcl  7272  oaass  7273  omlimcl  7290  findcard3  7823  frfi  7825  unblem1  7832  ordiso2  8039  inf3lem3  8144  r1sdom  8253  tz9.12lem3  8268  karden  8374  infxpenlem  8452  cardinfima  8535  iunfictbso  8552  dfac5  8566  cfflb  8696  cfcoflem  8709  cfcof  8711  fin23lem11  8754  fin23lem30  8779  fin1a2lem13  8849  axdc3lem2  8888  konigthlem  9000  alephval2  9004  pwcfsdom  9015  fpwwe2lem12  9073  tskuni  9215  axgroth6  9260  nqereu  9361  genpnmax  9439  ltaddpr  9466  recexsrlem  9534  mulgt0sr  9536  recexsr  9538  axrrecex  9594  axpre-sup  9600  addid1  9820  addid2  9823  recex  10251  zdiv  11013  btwnz  11044  lbzbi  11259  qbtwnre  11499  caubnd  13421  divalglem9  14380  divalglem9OLD  14381  unbenlem  14851  firest  15330  imasmnd2  16572  imasgrp2  16800  pmtrfrn  17098  pgpfi  17256  sylow2blem3  17273  imasring  17846  lspsneq  18344  lspdisj  18347  unitgOLD  19981  fctop  20017  cctop  20019  elcls  20087  elcls3  20097  subbascn  20268  cmpsublem  20412  cmpsub  20413  nllyidm  20502  comppfsc  20545  ptpjopn  20625  fbfinnfr  20854  filin  20867  isfil2  20869  infil  20876  fgss2  20887  fgfil  20888  fgcl  20891  fgabs  20892  elfm2  20961  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem4  20970  fmco  20974  flffbas  21008  cnpflf2  21013  fclscf  21038  alexsubALTlem2  21061  alexsubALTlem3  21062  alexsubALTlem4  21063  alexsubALT  21064  neibl  21514  met2ndc  21536  metcnp3  21553  icccmplem2  21839  xrge0tsms  21850  fgcfil  22239  volfiniun  22498  dyadmax  22554  dyadmbllem  22555  c1liplem1  22946  dgrlem  23181  axcontlem10  25001  usgrarnedg  25109  erclwwlksym  25540  erclwwlknsym  25552  lpni  25909  grpoidinvlem3  25932  grporcan  25947  grpoinvf  25966  nmosetre  26403  omlsii  27054  spansncol  27219  spansnss  27222  normcan  27227  spanunsni  27230  h1datomi  27232  nmopsetretALT  27514  nmfnsetre  27528  branmfn  27756  superpos  28005  chjatom  28008  cvbr4i  28018  atomli  28033  xrge0tsmsd  28556  eulerpartlemgh  29219  dfon2lem6  30441  trpredrec  30486  colineardim1  30833  finminlem  30979  nn0prpwlem  30983  neibastop2lem  31021  neibastop2  31022  fgmin  31031  heiborlem10  32116  prtlem15  32415  lshpcmp  32523  lsatn0  32534  lsatcmp  32538  lsmsat  32543  lsatcv0  32566  l1cvpat  32589  eqlkr  32634  lshpkrlem1  32645  lshpkrlem6  32650  lfl1dim  32656  lfl1dim2N  32657  lkrss2N  32704  athgt  32990  3dim2  33002  llnle  33052  llncmp  33056  lplnle  33074  lplnnle2at  33075  llncvrlpln2  33091  llncvrlpln  33092  lplncmp  33096  lplnexllnN  33098  lvolnle3at  33116  lplncvrlvol2  33149  lplncvrlvol  33150  lvolcmp  33151  pointpsubN  33285  pclfinN  33434  pclfinclN  33484  osumcllem11N  33500  pexmidlem4N  33507  cdleme17d3  34032  cdlemeg46gfre  34068  cdleme48gfv1  34072  cdleme50trn2  34087  trlord  34105  cdlemg6e  34158  cdlemj3  34359  diaelrnN  34582  diaintclN  34595  dia2dimlem6  34606  cdlemm10N  34655  dibintclN  34704  dihord6apre  34793  dihord5b  34796  dihord5apre  34799  dihglblem5apreN  34828  dihglblem2N  34831  dihglblem3N  34832  dihglbcpreN  34837  dihintcl  34881  lclkrlem2y  35068  lcfrvalsnN  35078  isnacs3  35521  jm2.26  35827  fnwe2lem2  35879  hbtlem5  35957  uzwo4  37365  disjinfi  37429  ssnnf1octb  37431  supxrgere  37510  supxrgelem  37514  suplesup  37516  islptre  37639  limcperiod  37648  limclner  37672  coskpi2  37681  cosknegpi  37684  icccncfext  37705  stoweidlem27  37827  stoweidlem59  37860  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem70  37980  fourierdlem71  37981  fourierdlem81  37991  fourierswlem  38034  sge0tsms  38130  sge0fsum  38137  sge0supre  38139  sge0sup  38141  sge0rnbnd  38143  sge0pnffigt  38146  sge0resrn  38154  sge0split  38159  sge0iunmptlemfi  38163  sge0rpcpnf  38171  sge0isum  38177  sge0xaddlem2  38184  sge0uzfsumgt  38194  nnfoctbdjlem  38201  nnfoctbdj  38202  meadjiunlem  38211  carageniuncllem2  38251  caratheodorylem2  38256  ovnsupge0  38283  ovncvrrp  38290  hoidmv1lelem3  38319  hoidmv1le  38320  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  ovnhoilem2  38328  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  bgoldbtbnd  38774  usgredg2vtx  39082  usgredg2vtxeuALT  39084  usgredgedga  39090  uhgrspan1  39144  nbuhgr2vtx1edgblem  39183  islindeps2  39897
  Copyright terms: Public domain W3C validator