Theorem rexlimdv 3136

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 3131	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 → (𝜑 → 𝜒))
4	3	com12 32	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexlimdva  3138  rexlimdva2  3140  rexlimdv3a  3142  rexlimdvw  3143  rexlimdvv  3193  rexlimdvvva  3195  elpwunsn  4628  onelssex  6372  eldmrexrnb  7044  weniso  7309  ssorduni  7733  onint  7744  limuni3  7803  peano5  7844  funcnvuni  7883  funeldmdif  8001  frxp  8076  smoiun  8301  tfrlem9  8324  oaordex  8493  oalimcl  8495  oaass  8496  findcard2  9099  findcard3  9193  frfi  9195  unblem1  9202  ordiso2  9430  inf3lem3  9551  r1sdom  9698  tz9.12lem3  9713  karden  9819  infxpenlem  9935  cardinfima  10019  iunfictbso  10036  dfac5  10051  cfcoflem  10194  fin23lem11  10239  fin23lem30  10264  fin1a2lem13  10334  axdc3lem2  10373  konigthlem  10491  fpwwe2lem11  10564  tskuni  10706  axgroth6  10751  nqereu  10852  genpnmax  10930  ltaddpr  10957  recexsrlem  11026  mulgt0sr  11028  axrrecex  11086  axpre-sup  11092  addrid  11326  addlid  11329  recex  11782  btwnz  12632  lbzbi  12886  qbtwnre  13151  caubnd  15321  divalglem9  16370  unbenlem  16879  firest  17395  imasmnd2  18742  imasgrp2  19031  pmtrfrn  19433  pgpfi  19580  sylow2blem3  19597  imasrng  20158  imasring  20310  lspsneq  21120  lspdisj  21123  elcls  23038  elcls3  23048  subbascn  23219  cmpsublem  23364  cmpsub  23365  nllyidm  23454  comppfsc  23497  ptpjopn  23577  fbfinnfr  23806  filin  23819  isfil2  23821  infil  23828  fgss2  23839  fgfil  23840  fgcl  23843  fgabs  23844  elfm2  23913  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fmco  23926  flffbas  23960  cnpflf2  23965  fclscf  23990  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  neibl  24466  met2ndc  24488  metcnp3  24505  icccmplem2  24789  xrge0tsms  24800  fgcfil  25238  volfiniun  25514  dyadmax  25565  dyadmbllem  25566  c1liplem1  25963  dgrlem  26194  axcontlem10  29042  usgredg2vtxeuALT  29291  ushgredgedg  29298  ushgredgedgloop  29300  uhgrspan1  29372  nbuhgr2vtx1edgblem  29420  erclwwlksym  30091  erclwwlknsym  30140  1pthon2v  30223  conngrv2edg  30265  lpni  30551  grpoidinvlem3  30577  grporcan  30589  omlsii  31474  spansncol  31639  spansnss  31642  spanunsni  31650  h1datomi  31652  nmopsetretALT  31934  branmfn  32176  chjatom  32428  cvbr4i  32438  atomli  32453  xrge0tsmsd  33134  umgr2cycllem  35322  umgr2cycl  35323  sat1el2xp  35561  fmlasuc  35568  satffunlem1lem2  35585  satffunlem2lem1  35586  satffunlem2lem2  35588  dfon2lem6  35968  colineardim1  36243  finminlem  36500  nn0prpwlem  36504  neibastop2lem  36542  neibastop2  36543  fgmin  36552  exrecfnlem  37695  heiborlem10  38141  prtlem15  39321  lshpcmp  39434  lsatn0  39445  lsatcmp  39449  lsmsat  39454  lsatcv0  39477  l1cvpat  39500  eqlkr  39545  lshpkrlem1  39556  lshpkrlem6  39561  lfl1dim  39567  lfl1dim2N  39568  lkrss2N  39615  athgt  39902  3dim2  39914  llnle  39964  llncmp  39968  lplnle  39986  lplnnle2at  39987  llncvrlpln2  40003  llncvrlpln  40004  lplncmp  40008  lplnexllnN  40010  lvolnle3at  40028  lplncvrlvol2  40061  lplncvrlvol  40062  lvolcmp  40063  pointpsubN  40197  pclfinN  40346  pclfinclN  40396  osumcllem11N  40412  pexmidlem4N  40419  cdleme17d3  40942  cdlemeg46gfre  40978  cdleme48gfv1  40982  cdleme50trn2  40997  trlord  41015  cdlemg6e  41068  cdlemj3  41269  diaelrnN  41491  diaintclN  41504  dia2dimlem6  41515  cdlemm10N  41564  dibintclN  41613  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dihglblem5apreN  41737  dihglblem2N  41740  dihglblem3N  41741  dihglbcpreN  41746  dihintcl  41790  lclkrlem2y  41977  lcfrvalsnN  41987  isnacs3  43142  jm2.26  43430  fnwe2lem2  43479  hbtlem5  43556  dflim5  43757  uzwo4  45484  iunincfi  45524  restuni3  45548  disjinfi  45622  ssnnf1octb  45624  choicefi  45629  mapssbi  45642  unirnmapsn  45643  iunmapsn  45646  supxrgere  45763  supxrgelem  45767  suplesup  45769  infleinf  45801  suplesup2  45805  rexabslelem  45846  islptre  46049  limcperiod  46058  limclner  46079  limsupmnfuzlem  46154  limsupre3lem  46160  coskpi2  46294  cosknegpi  46297  icccncfext  46315  stoweidlem27  46455  stoweidlem59  46487  fourierdlem41  46576  fourierdlem42  46577  fourierdlem70  46604  fourierdlem71  46605  fourierdlem81  46615  fourierswlem  46658  qndenserrnopnlem  46725  subsaliuncl  46786  subsalsal  46787  sge0tsms  46808  sge0fsum  46815  sge0supre  46817  sge0sup  46819  sge0rnbnd  46821  sge0pnffigt  46824  sge0resrn  46832  sge0split  46837  sge0iunmptlemfi  46841  sge0rpcpnf  46849  sge0isum  46855  sge0xaddlem2  46862  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  nnfoctbdjlem  46883  nnfoctbdj  46884  meadjiunlem  46893  meaiuninclem  46908  carageniuncllem2  46950  caratheodorylem2  46955  ovnsupge0  46985  ovncvrrp  46992  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem2  47030  opnvonmbllem2  47061  ovnovollem3  47086  sssmf  47166  smfpimbor1lem1  47226  smfco  47230  smfpimcc  47236  smfinflem  47245  nprmmul3  47989  fmtno4prmfac  48035  sfprmdvdsmersenne  48066  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbnd  48285  grimuhgr  48363  clnbgrgrim  48410  uspgrlimlem2  48465