Theorem rexlimdv 3283

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

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

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 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  rexlimdva  3284  rexlimdv3a  3286  rexlimdva2  3287  rexlimdvw  3290  rexlimdvv  3293  elpwunsn  4621  eldmrexrnb  6858  weniso  7107  ssorduni  7500  onint  7510  limuni3  7567  funcnvuni  7636  funeldmdif  7747  frxp  7820  smoiun  7998  tfrlem9  8021  oaordex  8184  oalimcl  8186  oaass  8187  findcard3  8761  frfi  8763  unblem1  8770  ordiso2  8979  inf3lem3  9093  r1sdom  9203  tz9.12lem3  9218  karden  9324  infxpenlem  9439  cardinfima  9523  iunfictbso  9540  dfac5  9554  cfcoflem  9694  fin23lem11  9739  fin23lem30  9764  fin1a2lem13  9834  axdc3lem2  9873  konigthlem  9990  fpwwe2lem12  10063  tskuni  10205  axgroth6  10250  nqereu  10351  genpnmax  10429  ltaddpr  10456  recexsrlem  10525  mulgt0sr  10527  axrrecex  10585  axpre-sup  10591  addid1  10820  addid2  10823  recex  11272  btwnz  12085  lbzbi  12337  qbtwnre  12593  caubnd  14718  divalglem9  15752  unbenlem  16244  firest  16706  imasmnd2  17948  imasgrp2  18214  pmtrfrn  18586  pgpfi  18730  sylow2blem3  18747  imasring  19369  lspsneq  19894  lspdisj  19897  elcls  21681  elcls3  21691  subbascn  21862  cmpsublem  22007  cmpsub  22008  nllyidm  22097  comppfsc  22140  ptpjopn  22220  fbfinnfr  22449  filin  22462  isfil2  22464  infil  22471  fgss2  22482  fgfil  22483  fgcl  22486  fgabs  22487  elfm2  22556  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  fmco  22569  flffbas  22603  cnpflf2  22608  fclscf  22633  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  neibl  23111  met2ndc  23133  metcnp3  23150  icccmplem2  23431  xrge0tsms  23442  fgcfil  23874  volfiniun  24148  dyadmax  24199  dyadmbllem  24200  c1liplem1  24593  dgrlem  24819  axcontlem10  26759  usgredg2vtxeuALT  27004  ushgredgedg  27011  ushgredgedgloop  27013  uhgrspan1  27085  nbuhgr2vtx1edgblem  27133  erclwwlksym  27799  erclwwlknsym  27849  1pthon2v  27932  conngrv2edg  27974  lpni  28257  grpoidinvlem3  28283  grporcan  28295  omlsii  29180  spansncol  29345  spansnss  29348  spanunsni  29356  h1datomi  29358  nmopsetretALT  29640  branmfn  29882  chjatom  30134  cvbr4i  30144  atomli  30159  xrge0tsmsd  30692  umgr2cycllem  32387  umgr2cycl  32388  sat1el2xp  32626  fmlasuc  32633  satffunlem1lem2  32650  satffunlem2lem1  32651  satffunlem2lem2  32653  dfon2lem6  33033  trpredrec  33077  colineardim1  33522  finminlem  33666  nn0prpwlem  33670  neibastop2lem  33708  neibastop2  33709  fgmin  33718  exrecfnlem  34663  heiborlem10  35113  prtlem15  36026  lshpcmp  36139  lsatn0  36150  lsatcmp  36154  lsmsat  36159  lsatcv0  36182  l1cvpat  36205  eqlkr  36250  lshpkrlem1  36261  lshpkrlem6  36266  lfl1dim  36272  lfl1dim2N  36273  lkrss2N  36320  athgt  36607  3dim2  36619  llnle  36669  llncmp  36673  lplnle  36691  lplnnle2at  36692  llncvrlpln2  36708  llncvrlpln  36709  lplncmp  36713  lplnexllnN  36715  lvolnle3at  36733  lplncvrlvol2  36766  lplncvrlvol  36767  lvolcmp  36768  pointpsubN  36902  pclfinN  37051  pclfinclN  37101  osumcllem11N  37117  pexmidlem4N  37124  cdleme17d3  37647  cdlemeg46gfre  37683  cdleme48gfv1  37687  cdleme50trn2  37702  trlord  37720  cdlemg6e  37773  cdlemj3  37974  diaelrnN  38196  diaintclN  38209  dia2dimlem6  38220  cdlemm10N  38269  dibintclN  38318  dihord6apre  38407  dihord5b  38410  dihord5apre  38413  dihglblem5apreN  38442  dihglblem2N  38445  dihglblem3N  38446  dihglbcpreN  38451  dihintcl  38495  lclkrlem2y  38682  lcfrvalsnN  38692  isnacs3  39356  jm2.26  39648  fnwe2lem2  39700  hbtlem5  39777  uzwo4  41364  iunincfi  41409  restuni3  41433  disjinfi  41503  ssnnf1octb  41505  choicefi  41512  mapssbi  41525  unirnmapsn  41526  ssmapsn  41528  iunmapsn  41529  supxrgere  41650  supxrgelem  41654  suplesup  41656  infleinf  41689  suplesup2  41693  rexabslelem  41741  islptre  41949  limcperiod  41958  limclner  41981  limsupmnfuzlem  42056  limsupre3lem  42062  coskpi2  42196  cosknegpi  42199  icccncfext  42219  stoweidlem27  42361  stoweidlem59  42393  fourierdlem41  42482  fourierdlem42  42483  fourierdlem70  42510  fourierdlem71  42511  fourierdlem81  42521  fourierswlem  42564  qndenserrnopnlem  42631  subsaliuncl  42690  subsalsal  42691  sge0tsms  42711  sge0fsum  42718  sge0supre  42720  sge0sup  42722  sge0rnbnd  42724  sge0pnffigt  42727  sge0resrn  42735  sge0split  42740  sge0iunmptlemfi  42744  sge0rpcpnf  42752  sge0isum  42758  sge0xaddlem2  42765  sge0uzfsumgt  42775  sge0seq  42777  sge0reuz  42778  nnfoctbdjlem  42786  nnfoctbdj  42787  meadjiunlem  42796  meaiuninclem  42811  carageniuncllem2  42853  caratheodorylem2  42858  ovnsupge0  42888  ovncvrrp  42895  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  ovnhoilem2  42933  opnvonmbllem2  42964  ovolval5lem3  42985  ovnovollem3  42989  sssmf  43064  smfpimbor1lem1  43122  smfco  43126  smfpimcc  43131  smfinflem  43140  fmtno4prmfac  43783  sfprmdvdsmersenne  43817  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbnd  44023