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

Theorem rexlimdv 2835
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.)
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 nfv 1673 . 2  |-  F/ x ph
2 nfv 1673 . 2  |-  F/ x ch
3 rexlimdv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
41, 2, 3rexlimd 2833 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  rexlimdva  2836  rexlimdv3a  2838  rexlimdvw  2839  rexlimdvv  2842  elpwunsn  3912  trintss  4396  eldmrexrnb  5845  dffo3  5853  weniso  6040  ssorduni  6392  onint  6401  limuni3  6458  funcnvuni  6525  frxp  6677  smoiun  6814  tfrlem9  6836  oaordex  6989  oalimcl  6991  oaass  6992  omlimcl  7009  fisucdomOLD  7508  findcard3  7547  frfi  7549  unblem1  7556  ordiso2  7721  inf3lem3  7828  noinfepOLD  7858  r1sdom  7973  tz9.12lem3  7988  karden  8094  infxpenlem  8172  cardinfima  8259  iunfictbso  8276  dfac5  8290  cfflb  8420  cfcoflem  8433  cfcof  8435  fin23lem11  8478  fin23lem30  8503  fin1a2lem13  8573  axdc3lem2  8612  konigthlem  8724  alephval2  8728  pwcfsdom  8739  fpwwe2lem12  8800  tskuni  8942  axgroth6  8987  nqereu  9090  genpnmax  9168  ltaddpr  9195  recexsrlem  9262  mulgt0sr  9264  recexsr  9266  axrrecex  9322  axpre-sup  9328  addid1  9541  addid2  9544  recex  9960  zdiv  10704  btwnz  10736  lbzbi  10935  qbtwnre  11161  caubnd  12838  divalglem9  13597  unbenlem  13961  firest  14363  imasmnd2  15450  imasgrp2  15661  pmtrfrn  15955  pgpfi  16095  sylow2blem3  16112  imasrng  16699  lspsneq  17180  lspdisj  17183  unitg  18547  fctop  18583  cctop  18585  elcls  18652  elcls3  18662  subbascn  18833  cmpsublem  18977  cmpsub  18978  nllyidm  19068  ptpjopn  19160  fbfinnfr  19389  filin  19402  isfil2  19404  infil  19411  fgss2  19422  fgfil  19423  fgcl  19426  fgabs  19427  elfm2  19496  rnelfm  19501  fmfnfmlem2  19503  fmfnfmlem4  19505  fmco  19509  flffbas  19543  cnpflf2  19548  fclscf  19573  alexsubALTlem2  19595  alexsubALTlem3  19596  alexsubALTlem4  19597  alexsubALT  19598  neibl  20051  met2ndc  20073  metcnp3  20090  icccmplem2  20375  xrge0tsms  20386  fgcfil  20757  volfiniun  21003  dyadmax  21053  dyadmbllem  21054  c1liplem1  21443  dgrlem  21672  axcontlem10  23170  usgrarnedg  23254  lpni  23617  grpoidinvlem3  23644  grpoidinvlem4  23645  grporcan  23659  grpoinvf  23678  nmosetre  24115  omlsii  24757  spansncol  24922  spansnss  24925  normcan  24930  spanunsni  24933  h1datomi  24935  nmopsetretALT  25218  nmfnsetre  25232  branmfn  25460  cnvbraval  25465  opsqrlem1  25495  superpos  25709  chjatom  25712  cvbr4i  25722  atomli  25737  xrge0tsmsd  26204  eulerpartlemgh  26713  dfon2lem6  27552  trpredrec  27653  colineardim1  28043  finminlem  28466  nn0prpwlem  28470  comppfsc  28532  neibastop2lem  28534  neibastop2  28535  fgmin  28544  heiborlem10  28672  prtlem15  28973  isnacs3  28999  jm2.26  29304  fnwe2lem2  29357  lnrfg  29428  hbtlem5  29437  climsuse  29734  stoweidlem27  29775  stoweidlem59  29807  erclwwlksym  30437  erclwwlknsym  30453  islindeps2  30906  lshpcmp  32473  lsatn0  32484  lsatcmp  32488  lsmsat  32493  lsatcv0  32516  l1cvpat  32539  eqlkr  32584  lshpkrlem1  32595  lshpkrlem6  32600  lfl1dim  32606  lfl1dim2N  32607  lkrss2N  32654  athgt  32940  3dim2  32952  llnle  33002  llncmp  33006  lplnle  33024  lplnnle2at  33025  llncvrlpln2  33041  llncvrlpln  33042  lplncmp  33046  lplnexllnN  33048  lvolnle3at  33066  lplncvrlvol2  33099  lplncvrlvol  33100  lvolcmp  33101  pointpsubN  33235  pclfinN  33384  pclfinclN  33434  osumcllem11N  33450  pexmidlem4N  33457  lhprelat3N  33524  cdleme17d3  33980  cdlemeg46gfre  34016  cdleme48gfv1  34020  cdleme50trn2  34035  trlord  34053  cdlemg6e  34106  cdlemj3  34307  diaelrnN  34530  diaintclN  34543  dia2dimlem6  34554  cdlemm10N  34603  dibintclN  34652  dihord6apre  34741  dihord5b  34744  dihord5apre  34747  dihglblem5apreN  34776  dihglblem2N  34779  dihglblem3N  34780  dihglbcpreN  34785  dihintcl  34829  lclkrlem2y  35016  lcfrvalsnN  35026
  Copyright terms: Public domain W3C validator