Theorem rexlimdv 3138

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  rexlimdva  3140  rexlimdva2  3142  rexlimdv3a  3144  rexlimdvw  3145  rexlimdvv  3195  rexlimdvvva  3197  elpwunsn  4616  onelssex  6359  eldmrexrnb  7033  weniso  7298  ssorduni  7722  onint  7733  limuni3  7792  peano5  7833  funcnvuni  7872  funeldmdif  7990  frxp  8066  smoiun  8291  tfrlem9  8314  oaordex  8483  oalimcl  8485  oaass  8486  findcard2  9089  findcard3  9183  frfi  9185  unblem1  9192  ordiso2  9420  inf3lem3  9542  r1sdom  9689  tz9.12lem3  9704  karden  9810  infxpenlem  9926  cardinfima  10010  iunfictbso  10027  dfac5  10042  cfcoflem  10185  fin23lem11  10230  fin23lem30  10255  fin1a2lem13  10325  axdc3lem2  10364  konigthlem  10482  fpwwe2lem11  10555  tskuni  10697  axgroth6  10742  nqereu  10843  genpnmax  10921  ltaddpr  10948  recexsrlem  11017  mulgt0sr  11019  axrrecex  11077  axpre-sup  11083  addrid  11317  addlid  11320  recex  11773  btwnz  12623  lbzbi  12877  qbtwnre  13142  caubnd  15312  divalglem9  16361  unbenlem  16870  firest  17386  imasmnd2  18733  imasgrp2  19022  pmtrfrn  19424  pgpfi  19571  sylow2blem3  19588  imasrng  20149  imasring  20301  lspsneq  21115  lspdisj  21118  elcls  23056  elcls3  23066  subbascn  23237  cmpsublem  23382  cmpsub  23383  nllyidm  23472  comppfsc  23515  ptpjopn  23595  fbfinnfr  23824  filin  23837  isfil2  23839  infil  23846  fgss2  23857  fgfil  23858  fgcl  23861  fgabs  23862  elfm2  23931  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem4  23940  fmco  23944  flffbas  23978  cnpflf2  23983  fclscf  24008  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  neibl  24484  met2ndc  24506  metcnp3  24523  icccmplem2  24807  xrge0tsms  24818  fgcfil  25256  volfiniun  25532  dyadmax  25583  dyadmbllem  25584  c1liplem1  25981  dgrlem  26212  axcontlem10  29060  usgredg2vtxeuALT  29309  ushgredgedg  29316  ushgredgedgloop  29318  uhgrspan1  29390  nbuhgr2vtx1edgblem  29438  erclwwlksym  30109  erclwwlknsym  30158  1pthon2v  30241  conngrv2edg  30283  lpni  30569  grpoidinvlem3  30595  grporcan  30607  omlsii  31492  spansncol  31657  spansnss  31660  spanunsni  31668  h1datomi  31670  nmopsetretALT  31952  branmfn  32194  chjatom  32446  cvbr4i  32456  atomli  32471  xrge0tsmsd  33154  umgr2cycllem  35368  umgr2cycl  35369  sat1el2xp  35607  fmlasuc  35614  satffunlem1lem2  35631  satffunlem2lem1  35632  satffunlem2lem2  35634  dfon2lem6  36014  colineardim1  36289  finminlem  36546  nn0prpwlem  36550  neibastop2lem  36588  neibastop2  36589  fgmin  36598  exrecfnlem  37741  heiborlem10  38187  prtlem15  39367  lshpcmp  39480  lsatn0  39491  lsatcmp  39495  lsmsat  39500  lsatcv0  39523  l1cvpat  39546  eqlkr  39591  lshpkrlem1  39602  lshpkrlem6  39607  lfl1dim  39613  lfl1dim2N  39614  lkrss2N  39661  athgt  39948  3dim2  39960  llnle  40010  llncmp  40014  lplnle  40032  lplnnle2at  40033  llncvrlpln2  40049  llncvrlpln  40050  lplncmp  40054  lplnexllnN  40056  lvolnle3at  40074  lplncvrlvol2  40107  lplncvrlvol  40108  lvolcmp  40109  pointpsubN  40243  pclfinN  40392  pclfinclN  40442  osumcllem11N  40458  pexmidlem4N  40465  cdleme17d3  40988  cdlemeg46gfre  41024  cdleme48gfv1  41028  cdleme50trn2  41043  trlord  41061  cdlemg6e  41114  cdlemj3  41315  diaelrnN  41537  diaintclN  41550  dia2dimlem6  41561  cdlemm10N  41610  dibintclN  41659  dihord6apre  41748  dihord5b  41751  dihord5apre  41754  dihglblem5apreN  41783  dihglblem2N  41786  dihglblem3N  41787  dihglbcpreN  41792  dihintcl  41836  lclkrlem2y  42023  lcfrvalsnN  42033  isnacs3  43159  jm2.26  43447  fnwe2lem2  43496  hbtlem5  43573  dflim5  43774  uzwo4  45501  iunincfi  45541  restuni3  45565  disjinfi  45639  ssnnf1octb  45641  choicefi  45646  mapssbi  45658  unirnmapsn  45659  iunmapsn  45662  supxrgere  45778  supxrgelem  45782  suplesup  45784  infleinf  45816  suplesup2  45820  rexabslelem  45861  islptre  46064  limcperiod  46073  limclner  46094  limsupmnfuzlem  46169  limsupre3lem  46175  coskpi2  46309  cosknegpi  46312  icccncfext  46330  stoweidlem27  46470  stoweidlem59  46502  fourierdlem41  46591  fourierdlem42  46592  fourierdlem70  46619  fourierdlem71  46620  fourierdlem81  46630  fourierswlem  46673  qndenserrnopnlem  46740  subsaliuncl  46801  subsalsal  46802  sge0tsms  46823  sge0fsum  46830  sge0supre  46832  sge0sup  46834  sge0rnbnd  46836  sge0pnffigt  46839  sge0resrn  46847  sge0split  46852  sge0iunmptlemfi  46856  sge0rpcpnf  46864  sge0isum  46870  sge0xaddlem2  46877  sge0uzfsumgt  46887  sge0seq  46889  sge0reuz  46890  nnfoctbdjlem  46898  nnfoctbdj  46899  meadjiunlem  46908  meaiuninclem  46923  carageniuncllem2  46965  caratheodorylem2  46970  ovnsupge0  47000  ovncvrrp  47007  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnhoilem2  47045  opnvonmbllem2  47076  ovnovollem3  47101  sssmf  47181  smfpimbor1lem1  47241  smfco  47245  smfpimcc  47251  smfinflem  47260  nprmmul3  48004  fmtno4prmfac  48050  sfprmdvdsmersenne  48081  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbnd  48300  grimuhgr  48378  clnbgrgrim  48425  uspgrlimlem2  48480