Theorem rexlimdv 3153

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexlimdva  3155  rexlimdva2  3157  rexlimdv3a  3159  rexlimdvw  3160  rexlimdvv  3210  elpwunsn  4687  onelssex  6412  eldmrexrnb  7093  weniso  7350  ssorduni  7765  onint  7777  limuni3  7840  peano5  7883  funcnvuni  7921  funeldmdif  8033  frxp  8111  smoiun  8360  tfrlem9  8384  oaordex  8557  oalimcl  8559  oaass  8560  findcard2  9163  findcard3  9284  findcard3OLD  9285  frfi  9287  unblem1  9294  ordiso2  9509  inf3lem3  9624  r1sdom  9768  tz9.12lem3  9783  karden  9889  infxpenlem  10007  cardinfima  10091  iunfictbso  10108  dfac5  10122  cfcoflem  10266  fin23lem11  10311  fin23lem30  10336  fin1a2lem13  10406  axdc3lem2  10445  konigthlem  10562  fpwwe2lem11  10635  tskuni  10777  axgroth6  10822  nqereu  10923  genpnmax  11001  ltaddpr  11028  recexsrlem  11097  mulgt0sr  11099  axrrecex  11157  axpre-sup  11163  addrid  11393  addlid  11396  recex  11845  btwnz  12664  lbzbi  12919  qbtwnre  13177  caubnd  15304  divalglem9  16343  unbenlem  16840  firest  17377  imasmnd2  18661  imasgrp2  18937  pmtrfrn  19325  pgpfi  19472  sylow2blem3  19489  imasring  20142  lspsneq  20734  lspdisj  20737  elcls  22576  elcls3  22586  subbascn  22757  cmpsublem  22902  cmpsub  22903  nllyidm  22992  comppfsc  23035  ptpjopn  23115  fbfinnfr  23344  filin  23357  isfil2  23359  infil  23366  fgss2  23377  fgfil  23378  fgcl  23381  fgabs  23382  elfm2  23451  rnelfm  23456  fmfnfmlem2  23458  fmfnfmlem4  23460  fmco  23464  flffbas  23498  cnpflf2  23503  fclscf  23528  alexsubALTlem2  23551  alexsubALTlem3  23552  alexsubALTlem4  23553  alexsubALT  23554  neibl  24009  met2ndc  24031  metcnp3  24048  icccmplem2  24338  xrge0tsms  24349  fgcfil  24787  volfiniun  25063  dyadmax  25114  dyadmbllem  25115  c1liplem1  25512  dgrlem  25742  axcontlem10  28228  usgredg2vtxeuALT  28476  ushgredgedg  28483  ushgredgedgloop  28485  uhgrspan1  28557  nbuhgr2vtx1edgblem  28605  erclwwlksym  29271  erclwwlknsym  29320  1pthon2v  29403  conngrv2edg  29445  lpni  29728  grpoidinvlem3  29754  grporcan  29766  omlsii  30651  spansncol  30816  spansnss  30819  spanunsni  30827  h1datomi  30829  nmopsetretALT  31111  branmfn  31353  chjatom  31605  cvbr4i  31615  atomli  31630  xrge0tsmsd  32204  umgr2cycllem  34126  umgr2cycl  34127  sat1el2xp  34365  fmlasuc  34372  satffunlem1lem2  34389  satffunlem2lem1  34390  satffunlem2lem2  34392  dfon2lem6  34755  colineardim1  35028  finminlem  35198  nn0prpwlem  35202  neibastop2lem  35240  neibastop2  35241  fgmin  35250  exrecfnlem  36255  heiborlem10  36683  prtlem15  37740  lshpcmp  37853  lsatn0  37864  lsatcmp  37868  lsmsat  37873  lsatcv0  37896  l1cvpat  37919  eqlkr  37964  lshpkrlem1  37975  lshpkrlem6  37980  lfl1dim  37986  lfl1dim2N  37987  lkrss2N  38034  athgt  38322  3dim2  38334  llnle  38384  llncmp  38388  lplnle  38406  lplnnle2at  38407  llncvrlpln2  38423  llncvrlpln  38424  lplncmp  38428  lplnexllnN  38430  lvolnle3at  38448  lplncvrlvol2  38481  lplncvrlvol  38482  lvolcmp  38483  pointpsubN  38617  pclfinN  38766  pclfinclN  38816  osumcllem11N  38832  pexmidlem4N  38839  cdleme17d3  39362  cdlemeg46gfre  39398  cdleme48gfv1  39402  cdleme50trn2  39417  trlord  39435  cdlemg6e  39488  cdlemj3  39689  diaelrnN  39911  diaintclN  39924  dia2dimlem6  39935  cdlemm10N  39984  dibintclN  40033  dihord6apre  40122  dihord5b  40125  dihord5apre  40128  dihglblem5apreN  40157  dihglblem2N  40160  dihglblem3N  40161  dihglbcpreN  40166  dihintcl  40210  lclkrlem2y  40397  lcfrvalsnN  40407  isnacs3  41438  jm2.26  41731  fnwe2lem2  41783  hbtlem5  41860  dflim5  42069  uzwo4  43730  iunincfi  43773  restuni3  43797  disjinfi  43881  ssnnf1octb  43883  choicefi  43889  mapssbi  43902  unirnmapsn  43903  ssmapsn  43905  iunmapsn  43906  supxrgere  44033  supxrgelem  44037  suplesup  44039  infleinf  44072  suplesup2  44076  rexabslelem  44118  islptre  44325  limcperiod  44334  limclner  44357  limsupmnfuzlem  44432  limsupre3lem  44438  coskpi2  44572  cosknegpi  44575  icccncfext  44593  stoweidlem27  44733  stoweidlem59  44765  fourierdlem41  44854  fourierdlem42  44855  fourierdlem70  44882  fourierdlem71  44883  fourierdlem81  44893  fourierswlem  44936  qndenserrnopnlem  45003  subsaliuncl  45064  subsalsal  45065  sge0tsms  45086  sge0fsum  45093  sge0supre  45095  sge0sup  45097  sge0rnbnd  45099  sge0pnffigt  45102  sge0resrn  45110  sge0split  45115  sge0iunmptlemfi  45119  sge0rpcpnf  45127  sge0isum  45133  sge0xaddlem2  45140  sge0uzfsumgt  45150  sge0seq  45152  sge0reuz  45153  nnfoctbdjlem  45161  nnfoctbdj  45162  meadjiunlem  45171  meaiuninclem  45186  carageniuncllem2  45228  caratheodorylem2  45233  ovnsupge0  45263  ovncvrrp  45270  hoidmv1lelem3  45299  hoidmv1le  45300  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  ovnhoilem2  45308  opnvonmbllem2  45339  ovnovollem3  45364  sssmf  45444  smfpimbor1lem1  45504  smfco  45508  smfpimcc  45514  smfinflem  45523  fmtno4prmfac  46230  sfprmdvdsmersenne  46261  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  bgoldbtbnd  46467  imasrng  46668