Theorem rexlimdv 3131

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	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		rexlimdv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
2	1	com3l 89	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜓 → (𝜑 → 𝜒)))
3	2	rexlimiv 3126	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 → (𝜑 → 𝜒))
4	3	com12 32	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimdva  3133  rexlimdva2  3135  rexlimdv3a  3137  rexlimdvw  3138  rexlimdvv  3188  rexlimdvvva  3190  elpwunsn  4637  onelssex  6355  eldmrexrnb  7025  weniso  7288  ssorduni  7712  onint  7723  limuni3  7782  peano5  7823  funcnvuni  7862  funeldmdif  7980  frxp  8056  smoiun  8281  tfrlem9  8304  oaordex  8473  oalimcl  8475  oaass  8476  findcard2  9074  findcard3  9167  frfi  9169  unblem1  9176  ordiso2  9401  inf3lem3  9520  r1sdom  9667  tz9.12lem3  9682  karden  9788  infxpenlem  9904  cardinfima  9988  iunfictbso  10005  dfac5  10020  cfcoflem  10163  fin23lem11  10208  fin23lem30  10233  fin1a2lem13  10303  axdc3lem2  10342  konigthlem  10459  fpwwe2lem11  10532  tskuni  10674  axgroth6  10719  nqereu  10820  genpnmax  10898  ltaddpr  10925  recexsrlem  10994  mulgt0sr  10996  axrrecex  11054  axpre-sup  11060  addrid  11293  addlid  11296  recex  11749  btwnz  12576  lbzbi  12834  qbtwnre  13098  caubnd  15266  divalglem9  16312  unbenlem  16820  firest  17336  imasmnd2  18682  imasgrp2  18968  pmtrfrn  19371  pgpfi  19518  sylow2blem3  19535  imasrng  20096  imasring  20249  lspsneq  21060  lspdisj  21063  elcls  22989  elcls3  22999  subbascn  23170  cmpsublem  23315  cmpsub  23316  nllyidm  23405  comppfsc  23448  ptpjopn  23528  fbfinnfr  23757  filin  23770  isfil2  23772  infil  23779  fgss2  23790  fgfil  23791  fgcl  23794  fgabs  23795  elfm2  23864  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  fmco  23877  flffbas  23911  cnpflf2  23916  fclscf  23941  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  alexsubALT  23967  neibl  24417  met2ndc  24439  metcnp3  24456  icccmplem2  24740  xrge0tsms  24751  fgcfil  25199  volfiniun  25476  dyadmax  25527  dyadmbllem  25528  c1liplem1  25929  dgrlem  26162  axcontlem10  28952  usgredg2vtxeuALT  29201  ushgredgedg  29208  ushgredgedgloop  29210  uhgrspan1  29282  nbuhgr2vtx1edgblem  29330  erclwwlksym  29999  erclwwlknsym  30048  1pthon2v  30131  conngrv2edg  30173  lpni  30458  grpoidinvlem3  30484  grporcan  30496  omlsii  31381  spansncol  31546  spansnss  31549  spanunsni  31557  h1datomi  31559  nmopsetretALT  31841  branmfn  32083  chjatom  32335  cvbr4i  32345  atomli  32360  xrge0tsmsd  33040  umgr2cycllem  35182  umgr2cycl  35183  sat1el2xp  35421  fmlasuc  35428  satffunlem1lem2  35445  satffunlem2lem1  35446  satffunlem2lem2  35448  dfon2lem6  35828  colineardim1  36101  finminlem  36358  nn0prpwlem  36362  neibastop2lem  36400  neibastop2  36401  fgmin  36410  exrecfnlem  37419  heiborlem10  37866  prtlem15  38920  lshpcmp  39033  lsatn0  39044  lsatcmp  39048  lsmsat  39053  lsatcv0  39076  l1cvpat  39099  eqlkr  39144  lshpkrlem1  39155  lshpkrlem6  39160  lfl1dim  39166  lfl1dim2N  39167  lkrss2N  39214  athgt  39501  3dim2  39513  llnle  39563  llncmp  39567  lplnle  39585  lplnnle2at  39586  llncvrlpln2  39602  llncvrlpln  39603  lplncmp  39607  lplnexllnN  39609  lvolnle3at  39627  lplncvrlvol2  39660  lplncvrlvol  39661  lvolcmp  39662  pointpsubN  39796  pclfinN  39945  pclfinclN  39995  osumcllem11N  40011  pexmidlem4N  40018  cdleme17d3  40541  cdlemeg46gfre  40577  cdleme48gfv1  40581  cdleme50trn2  40596  trlord  40614  cdlemg6e  40667  cdlemj3  40868  diaelrnN  41090  diaintclN  41103  dia2dimlem6  41114  cdlemm10N  41163  dibintclN  41212  dihord6apre  41301  dihord5b  41304  dihord5apre  41307  dihglblem5apreN  41336  dihglblem2N  41339  dihglblem3N  41340  dihglbcpreN  41345  dihintcl  41389  lclkrlem2y  41576  lcfrvalsnN  41586  isnacs3  42749  jm2.26  43041  fnwe2lem2  43090  hbtlem5  43167  dflim5  43368  uzwo4  45096  iunincfi  45137  restuni3  45161  disjinfi  45235  ssnnf1octb  45237  choicefi  45243  mapssbi  45256  unirnmapsn  45257  iunmapsn  45260  supxrgere  45378  supxrgelem  45382  suplesup  45384  infleinf  45416  suplesup2  45420  rexabslelem  45462  islptre  45665  limcperiod  45674  limclner  45695  limsupmnfuzlem  45770  limsupre3lem  45776  coskpi2  45910  cosknegpi  45913  icccncfext  45931  stoweidlem27  46071  stoweidlem59  46103  fourierdlem41  46192  fourierdlem42  46193  fourierdlem70  46220  fourierdlem71  46221  fourierdlem81  46231  fourierswlem  46274  qndenserrnopnlem  46341  subsaliuncl  46402  subsalsal  46403  sge0tsms  46424  sge0fsum  46431  sge0supre  46433  sge0sup  46435  sge0rnbnd  46437  sge0pnffigt  46440  sge0resrn  46448  sge0split  46453  sge0iunmptlemfi  46457  sge0rpcpnf  46465  sge0isum  46471  sge0xaddlem2  46478  sge0uzfsumgt  46488  sge0seq  46490  sge0reuz  46491  nnfoctbdjlem  46499  nnfoctbdj  46500  meadjiunlem  46509  meaiuninclem  46524  carageniuncllem2  46566  caratheodorylem2  46571  ovnsupge0  46601  ovncvrrp  46608  hoidmv1lelem3  46637  hoidmv1le  46638  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem3  46641  ovnhoilem2  46646  opnvonmbllem2  46677  ovnovollem3  46702  sssmf  46782  smfpimbor1lem1  46842  smfco  46846  smfpimcc  46852  smfinflem  46861  fmtno4prmfac  47609  sfprmdvdsmersenne  47640  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  bgoldbtbnd  47846  grimuhgr  47924  clnbgrgrim  47971  uspgrlimlem2  48026