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

Theorem rexlimdv 2922
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 2918 . 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 1870   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  rexlimdva  2924  rexlimdv3a  2926  rexlimdvw  2927  rexlimdvv  2930  elpwunsn  4043  trintss  4536  eldmrexrnb  6044  dffo3  6052  weniso  6260  ssorduni  6626  onint  6636  limuni3  6693  funcnvuni  6760  frxp  6917  smoiun  7088  tfrlem9  7111  oaordex  7267  oalimcl  7269  oaass  7270  omlimcl  7287  findcard3  7820  frfi  7822  unblem1  7829  ordiso2  8030  inf3lem3  8135  r1sdom  8244  tz9.12lem3  8259  karden  8365  infxpenlem  8443  cardinfima  8526  iunfictbso  8543  dfac5  8557  cfflb  8687  cfcoflem  8700  cfcof  8702  fin23lem11  8745  fin23lem30  8770  fin1a2lem13  8840  axdc3lem2  8879  konigthlem  8991  alephval2  8995  pwcfsdom  9006  fpwwe2lem12  9065  tskuni  9207  axgroth6  9252  nqereu  9353  genpnmax  9431  ltaddpr  9458  recexsrlem  9526  mulgt0sr  9528  recexsr  9530  axrrecex  9586  axpre-sup  9592  addid1  9812  addid2  9815  recex  10243  zdiv  11006  btwnz  11037  lbzbi  11252  qbtwnre  11492  caubnd  13400  divalglem9  14357  unbenlem  14806  firest  15281  imasmnd2  16515  imasgrp2  16743  pmtrfrn  17041  pgpfi  17183  sylow2blem3  17200  imasring  17773  lspsneq  18271  lspdisj  18274  unitgOLD  19905  fctop  19941  cctop  19943  elcls  20011  elcls3  20021  subbascn  20192  cmpsublem  20336  cmpsub  20337  nllyidm  20426  comppfsc  20469  ptpjopn  20549  fbfinnfr  20778  filin  20791  isfil2  20793  infil  20800  fgss2  20811  fgfil  20812  fgcl  20815  fgabs  20816  elfm2  20885  rnelfm  20890  fmfnfmlem2  20892  fmfnfmlem4  20894  fmco  20898  flffbas  20932  cnpflf2  20937  fclscf  20962  alexsubALTlem2  20985  alexsubALTlem3  20986  alexsubALTlem4  20987  alexsubALT  20988  neibl  21438  met2ndc  21460  metcnp3  21477  icccmplem2  21743  xrge0tsms  21754  fgcfil  22125  volfiniun  22368  dyadmax  22424  dyadmbllem  22425  c1liplem1  22816  dgrlem  23042  axcontlem10  24840  usgrarnedg  24948  erclwwlksym  25378  erclwwlknsym  25390  lpni  25747  grpoidinvlem3  25770  grporcan  25785  grpoinvf  25804  nmosetre  26241  omlsii  26882  spansncol  27047  spansnss  27050  normcan  27055  spanunsni  27058  h1datomi  27060  nmopsetretALT  27342  nmfnsetre  27356  branmfn  27584  superpos  27833  chjatom  27836  cvbr4i  27846  atomli  27861  xrge0tsmsd  28378  eulerpartlemgh  29028  dfon2lem6  30212  trpredrec  30257  colineardim1  30604  finminlem  30750  nn0prpwlem  30754  neibastop2lem  30792  neibastop2  30793  fgmin  30802  heiborlem10  31846  prtlem15  32145  lshpcmp  32253  lsatn0  32264  lsatcmp  32268  lsmsat  32273  lsatcv0  32296  l1cvpat  32319  eqlkr  32364  lshpkrlem1  32375  lshpkrlem6  32380  lfl1dim  32386  lfl1dim2N  32387  lkrss2N  32434  athgt  32720  3dim2  32732  llnle  32782  llncmp  32786  lplnle  32804  lplnnle2at  32805  llncvrlpln2  32821  llncvrlpln  32822  lplncmp  32826  lplnexllnN  32828  lvolnle3at  32846  lplncvrlvol2  32879  lplncvrlvol  32880  lvolcmp  32881  pointpsubN  33015  pclfinN  33164  pclfinclN  33214  osumcllem11N  33230  pexmidlem4N  33237  cdleme17d3  33762  cdlemeg46gfre  33798  cdleme48gfv1  33802  cdleme50trn2  33817  trlord  33835  cdlemg6e  33888  cdlemj3  34089  diaelrnN  34312  diaintclN  34325  dia2dimlem6  34336  cdlemm10N  34385  dibintclN  34434  dihord6apre  34523  dihord5b  34526  dihord5apre  34529  dihglblem5apreN  34558  dihglblem2N  34561  dihglblem3N  34562  dihglbcpreN  34567  dihintcl  34611  lclkrlem2y  34798  lcfrvalsnN  34808  isnacs3  35251  jm2.26  35553  fnwe2lem2  35605  hbtlem5  35683  uzwo4  37023  disjinfi  37081  supxrgere  37155  supxrgelem  37159  suplesup  37161  islptre  37261  limcperiod  37270  limclner  37294  coskpi2  37303  cosknegpi  37306  icccncfext  37327  stoweidlem27  37446  stoweidlem59  37479  fourierdlem41  37569  fourierdlem42  37570  fourierdlem70  37598  fourierdlem71  37599  fourierdlem81  37609  fourierswlem  37652  sge0tsms  37746  sge0fsum  37753  sge0supre  37755  sge0sup  37757  sge0rnbnd  37759  sge0pnffigt  37762  sge0resrn  37770  sge0split  37775  sge0iunmptlemfi  37779  nnfoctbdjlem  37792  nnfoctbdj  37793  meadjiunlem  37802  carageniuncllem2  37842  caratheodorylem2  37847  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbnd  38284  islindeps2  39026
  Copyright terms: Public domain W3C validator