Theorem rexlimdv 3030

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

Step	Hyp	Ref	Expression
1		rexlimdv.1	. . . 4 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
2	1	com3l 89	. . 3 |- ( x e. A -> ( ps -> ( ph -> ch ) ) )
3	2	rexlimiv 3027	. 2 |- ( E. x e. A ps -> ( ph -> ch ) )
4	3	com12 32	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexlimdva  3031  rexlimdv3a  3033  rexlimdvw  3034  rexlimdvv  3037  elpwunsn  4224  trintssOLD  4770  eldmrexrnb  6366  dffo3  6374  weniso  6604  ssorduni  6985  onint  6995  limuni3  7052  funcnvuni  7119  frxp  7287  smoiun  7458  tfrlem9  7481  oaordex  7638  oalimcl  7640  oaass  7641  omlimcl  7658  findcard3  8203  frfi  8205  unblem1  8212  ordiso2  8420  inf3lem3  8527  r1sdom  8637  tz9.12lem3  8652  karden  8758  infxpenlem  8836  cardinfima  8920  iunfictbso  8937  dfac5  8951  cfflb  9081  cfcoflem  9094  cfcof  9096  fin23lem11  9139  fin23lem30  9164  fin1a2lem13  9234  axdc3lem2  9273  konigthlem  9390  alephval2  9394  pwcfsdom  9405  fpwwe2lem12  9463  tskuni  9605  axgroth6  9650  nqereu  9751  genpnmax  9829  ltaddpr  9856  recexsrlem  9924  mulgt0sr  9926  recexsr  9928  axrrecex  9984  axpre-sup  9990  addid1  10216  addid2  10219  recex  10659  zdiv  11447  btwnz  11479  lbzbi  11776  qbtwnre  12030  caubnd  14098  divalglem9  15124  unbenlem  15612  firest  16093  imasmnd2  17327  imasgrp2  17530  pmtrfrn  17878  pgpfi  18020  sylow2blem3  18037  imasring  18619  lspsneq  19122  lspdisj  19125  fctop  20808  cctop  20810  elcls  20877  elcls3  20887  subbascn  21058  cmpsublem  21202  cmpsub  21203  nllyidm  21292  comppfsc  21335  ptpjopn  21415  fbfinnfr  21645  filin  21658  isfil2  21660  infil  21667  fgss2  21678  fgfil  21679  fgcl  21682  fgabs  21683  elfm2  21752  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmco  21765  flffbas  21799  cnpflf2  21804  fclscf  21829  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  neibl  22306  met2ndc  22328  metcnp3  22345  icccmplem2  22626  xrge0tsms  22637  fgcfil  23069  volfiniun  23315  dyadmax  23366  dyadmbllem  23367  c1liplem1  23759  dgrlem  23985  axcontlem10  25853  usgredg2vtxeuALT  26114  ushgredgedg  26121  ushgredgedgloop  26123  uhgrspan1  26195  nbuhgr2vtx1edgblem  26247  erclwwlkssym  26935  erclwwlksnsym  26947  1pthon2v  27013  conngrv2edg  27055  lpni  27332  grpoidinvlem3  27360  grporcan  27372  grpoinvf  27386  nmosetre  27619  omlsii  28262  spansncol  28427  spansnss  28430  normcan  28435  spanunsni  28438  h1datomi  28440  nmopsetretALT  28722  nmfnsetre  28736  branmfn  28964  superpos  29213  chjatom  29216  cvbr4i  29226  atomli  29241  xrge0tsmsd  29785  eulerpartlemgh  30440  dfon2lem6  31693  trpredrec  31738  colineardim1  32168  finminlem  32312  nn0prpwlem  32317  neibastop2lem  32355  neibastop2  32356  fgmin  32365  heiborlem10  33619  prtlem15  34160  lshpcmp  34275  lsatn0  34286  lsatcmp  34290  lsmsat  34295  lsatcv0  34318  l1cvpat  34341  eqlkr  34386  lshpkrlem1  34397  lshpkrlem6  34402  lfl1dim  34408  lfl1dim2N  34409  lkrss2N  34456  athgt  34742  3dim2  34754  llnle  34804  llncmp  34808  lplnle  34826  lplnnle2at  34827  llncvrlpln2  34843  llncvrlpln  34844  lplncmp  34848  lplnexllnN  34850  lvolnle3at  34868  lplncvrlvol2  34901  lplncvrlvol  34902  lvolcmp  34903  pointpsubN  35037  pclfinN  35186  pclfinclN  35236  osumcllem11N  35252  pexmidlem4N  35259  cdleme17d3  35784  cdlemeg46gfre  35820  cdleme48gfv1  35824  cdleme50trn2  35839  trlord  35857  cdlemg6e  35910  cdlemj3  36111  diaelrnN  36334  diaintclN  36347  dia2dimlem6  36358  cdlemm10N  36407  dibintclN  36456  dihord6apre  36545  dihord5b  36548  dihord5apre  36551  dihglblem5apreN  36580  dihglblem2N  36583  dihglblem3N  36584  dihglbcpreN  36589  dihintcl  36633  lclkrlem2y  36820  lcfrvalsnN  36830  isnacs3  37273  jm2.26  37569  fnwe2lem2  37621  hbtlem5  37698  uzwo4  39221  iunincfi  39272  restuni3  39301  rexlimdva2  39339  disjinfi  39380  ssnnf1octb  39382  mapsnd  39388  choicefi  39392  mapssbi  39405  unirnmapsn  39406  ssmapsn  39408  iunmapsn  39409  supxrgere  39549  supxrgelem  39553  suplesup  39555  infleinf  39588  suplesup2  39592  rexabslelem  39645  islptre  39851  limcperiod  39860  limclner  39883  limsupubuz  39945  limsupmnfuzlem  39958  limsupre3lem  39964  coskpi2  40077  cosknegpi  40080  icccncfext  40100  stoweidlem27  40244  stoweidlem59  40276  fourierdlem41  40365  fourierdlem42  40366  fourierdlem70  40393  fourierdlem71  40394  fourierdlem81  40404  fourierswlem  40447  qndenserrnopnlem  40517  subsaliuncl  40576  subsalsal  40577  sge0tsms  40597  sge0fsum  40604  sge0supre  40606  sge0sup  40608  sge0rnbnd  40610  sge0pnffigt  40613  sge0resrn  40621  sge0split  40626  sge0iunmptlemfi  40630  sge0rpcpnf  40638  sge0isum  40644  sge0xaddlem2  40651  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  nnfoctbdjlem  40672  nnfoctbdj  40673  meadjiunlem  40682  meaiuninclem  40697  carageniuncllem2  40736  caratheodorylem2  40741  ovnsupge0  40771  ovncvrrp  40778  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem2  40816  opnvonmbllem2  40847  ovolval5lem3  40868  ovnovollem3  40872  sssmf  40947  smflimlem4  40982  smfpimbor1lem1  41005  smfco  41009  smfpimcc  41014  smfinflem  41023  fmtno4prmfac  41484  sfprmdvdsmersenne  41520  mogoldbb  41673  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbnd  41697  islindeps2  42272