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

Theorem rexlimdv 2870
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 83 . . 3  |-  ( x  e.  A  ->  ( ps  ->  ( ph  ->  ch ) ) )
32rexlimiv 2867 . 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 1904   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-ral 2761  df-rex 2762
This theorem is referenced by:  rexlimdva  2871  rexlimdv3a  2873  rexlimdvw  2874  rexlimdvv  2877  elpwunsn  4003  trintss  4506  eldmrexrnb  6044  dffo3  6052  weniso  6263  ssorduni  6631  onint  6641  limuni3  6698  funcnvuni  6765  frxp  6925  smoiun  7098  tfrlem9  7121  oaordex  7277  oalimcl  7279  oaass  7280  omlimcl  7297  findcard3  7832  frfi  7834  unblem1  7841  ordiso2  8048  inf3lem3  8153  r1sdom  8263  tz9.12lem3  8278  karden  8384  infxpenlem  8462  cardinfima  8546  iunfictbso  8563  dfac5  8577  cfflb  8707  cfcoflem  8720  cfcof  8722  fin23lem11  8765  fin23lem30  8790  fin1a2lem13  8860  axdc3lem2  8899  konigthlem  9011  alephval2  9015  pwcfsdom  9026  fpwwe2lem12  9084  tskuni  9226  axgroth6  9271  nqereu  9372  genpnmax  9450  ltaddpr  9477  recexsrlem  9545  mulgt0sr  9547  recexsr  9549  axrrecex  9605  axpre-sup  9611  addid1  9831  addid2  9834  recex  10266  zdiv  11029  btwnz  11060  lbzbi  11275  qbtwnre  11515  caubnd  13498  divalglem9  14460  divalglem9OLD  14461  unbenlem  14931  firest  15409  imasmnd2  16651  imasgrp2  16879  pmtrfrn  17177  pgpfi  17335  sylow2blem3  17352  imasring  17925  lspsneq  18423  lspdisj  18426  unitgOLD  20060  fctop  20096  cctop  20098  elcls  20166  elcls3  20176  subbascn  20347  cmpsublem  20491  cmpsub  20492  nllyidm  20581  comppfsc  20624  ptpjopn  20704  fbfinnfr  20934  filin  20947  isfil2  20949  infil  20956  fgss2  20967  fgfil  20968  fgcl  20971  fgabs  20972  elfm2  21041  rnelfm  21046  fmfnfmlem2  21048  fmfnfmlem4  21050  fmco  21054  flffbas  21088  cnpflf2  21093  fclscf  21118  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALTlem4  21143  alexsubALT  21144  neibl  21594  met2ndc  21616  metcnp3  21633  icccmplem2  21919  xrge0tsms  21930  fgcfil  22319  volfiniun  22579  dyadmax  22635  dyadmbllem  22636  c1liplem1  23027  dgrlem  23262  axcontlem10  25082  usgrarnedg  25190  erclwwlksym  25621  erclwwlknsym  25633  lpni  25990  grpoidinvlem3  26015  grporcan  26030  grpoinvf  26049  nmosetre  26486  omlsii  27137  spansncol  27302  spansnss  27305  normcan  27310  spanunsni  27313  h1datomi  27315  nmopsetretALT  27597  nmfnsetre  27611  branmfn  27839  superpos  28088  chjatom  28091  cvbr4i  28101  atomli  28116  xrge0tsmsd  28622  eulerpartlemgh  29284  dfon2lem6  30505  trpredrec  30550  colineardim1  30899  finminlem  31045  nn0prpwlem  31049  neibastop2lem  31087  neibastop2  31088  fgmin  31097  heiborlem10  32216  prtlem15  32511  lshpcmp  32625  lsatn0  32636  lsatcmp  32640  lsmsat  32645  lsatcv0  32668  l1cvpat  32691  eqlkr  32736  lshpkrlem1  32747  lshpkrlem6  32752  lfl1dim  32758  lfl1dim2N  32759  lkrss2N  32806  athgt  33092  3dim2  33104  llnle  33154  llncmp  33158  lplnle  33176  lplnnle2at  33177  llncvrlpln2  33193  llncvrlpln  33194  lplncmp  33198  lplnexllnN  33200  lvolnle3at  33218  lplncvrlvol2  33251  lplncvrlvol  33252  lvolcmp  33253  pointpsubN  33387  pclfinN  33536  pclfinclN  33586  osumcllem11N  33602  pexmidlem4N  33609  cdleme17d3  34134  cdlemeg46gfre  34170  cdleme48gfv1  34174  cdleme50trn2  34189  trlord  34207  cdlemg6e  34260  cdlemj3  34461  diaelrnN  34684  diaintclN  34697  dia2dimlem6  34708  cdlemm10N  34757  dibintclN  34806  dihord6apre  34895  dihord5b  34898  dihord5apre  34901  dihglblem5apreN  34930  dihglblem2N  34933  dihglblem3N  34934  dihglbcpreN  34939  dihintcl  34983  lclkrlem2y  35170  lcfrvalsnN  35180  isnacs3  35623  jm2.26  35928  fnwe2lem2  35980  hbtlem5  36058  uzwo4  37451  disjinfi  37539  ssnnf1octb  37541  mapsnd  37547  choicefi  37552  mapssbi  37566  unirnmapsn  37567  ssmapsn  37569  iunmapsn  37570  supxrgere  37643  supxrgelem  37647  suplesup  37649  infleinf  37682  islptre  37796  limcperiod  37805  limclner  37829  coskpi2  37838  cosknegpi  37841  icccncfext  37862  stoweidlem27  37999  stoweidlem59  38032  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem70  38152  fourierdlem71  38153  fourierdlem81  38163  fourierswlem  38206  qndenserrnopnlem  38278  sge0tsms  38336  sge0fsum  38343  sge0supre  38345  sge0sup  38347  sge0rnbnd  38349  sge0pnffigt  38352  sge0resrn  38360  sge0split  38365  sge0iunmptlemfi  38369  sge0rpcpnf  38377  sge0isum  38383  sge0xaddlem2  38390  sge0uzfsumgt  38400  sge0seq  38402  nnfoctbdjlem  38409  nnfoctbdj  38410  meadjiunlem  38419  carageniuncllem2  38462  caratheodorylem2  38467  ovnsupge0  38497  ovncvrrp  38504  hoidmv1lelem3  38533  hoidmv1le  38534  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem3  38537  ovnhoilem2  38542  opnvonmbllem2  38573  ovolval5lem3  38594  ovnovollem3  38598  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbnd  39049  usgredg2vtxeuALT  39463  ushgredgedga  39470  ushgredgedgaloop  39472  uhgrspan1  39539  nbuhgr2vtx1edgblem  39583  1pthon2v-av  40041  islindeps2  40784
  Copyright terms: Public domain W3C validator