Theorem rexlimdv 3154

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimdva  3156  rexlimdva2  3158  rexlimdv3a  3160  rexlimdvw  3161  rexlimdvv  3211  elpwunsn  4688  onelssex  6413  eldmrexrnb  7094  weniso  7351  ssorduni  7766  onint  7778  limuni3  7841  peano5  7884  funcnvuni  7922  funeldmdif  8034  frxp  8112  smoiun  8361  tfrlem9  8385  oaordex  8558  oalimcl  8560  oaass  8561  findcard2  9164  findcard3  9285  findcard3OLD  9286  frfi  9288  unblem1  9295  ordiso2  9510  inf3lem3  9625  r1sdom  9769  tz9.12lem3  9784  karden  9890  infxpenlem  10008  cardinfima  10092  iunfictbso  10109  dfac5  10123  cfcoflem  10267  fin23lem11  10312  fin23lem30  10337  fin1a2lem13  10407  axdc3lem2  10446  konigthlem  10563  fpwwe2lem11  10636  tskuni  10778  axgroth6  10823  nqereu  10924  genpnmax  11002  ltaddpr  11029  recexsrlem  11098  mulgt0sr  11100  axrrecex  11158  axpre-sup  11164  addrid  11394  addlid  11397  recex  11846  btwnz  12665  lbzbi  12920  qbtwnre  13178  caubnd  15305  divalglem9  16344  unbenlem  16841  firest  17378  imasmnd2  18662  imasgrp2  18938  pmtrfrn  19326  pgpfi  19473  sylow2blem3  19490  imasring  20143  lspsneq  20735  lspdisj  20738  elcls  22577  elcls3  22587  subbascn  22758  cmpsublem  22903  cmpsub  22904  nllyidm  22993  comppfsc  23036  ptpjopn  23116  fbfinnfr  23345  filin  23358  isfil2  23360  infil  23367  fgss2  23378  fgfil  23379  fgcl  23382  fgabs  23383  elfm2  23452  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  fmco  23465  flffbas  23499  cnpflf2  23504  fclscf  23529  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  neibl  24010  met2ndc  24032  metcnp3  24049  icccmplem2  24339  xrge0tsms  24350  fgcfil  24788  volfiniun  25064  dyadmax  25115  dyadmbllem  25116  c1liplem1  25513  dgrlem  25743  axcontlem10  28231  usgredg2vtxeuALT  28479  ushgredgedg  28486  ushgredgedgloop  28488  uhgrspan1  28560  nbuhgr2vtx1edgblem  28608  erclwwlksym  29274  erclwwlknsym  29323  1pthon2v  29406  conngrv2edg  29448  lpni  29733  grpoidinvlem3  29759  grporcan  29771  omlsii  30656  spansncol  30821  spansnss  30824  spanunsni  30832  h1datomi  30834  nmopsetretALT  31116  branmfn  31358  chjatom  31610  cvbr4i  31620  atomli  31635  xrge0tsmsd  32209  umgr2cycllem  34131  umgr2cycl  34132  sat1el2xp  34370  fmlasuc  34377  satffunlem1lem2  34394  satffunlem2lem1  34395  satffunlem2lem2  34397  dfon2lem6  34760  colineardim1  35033  finminlem  35203  nn0prpwlem  35207  neibastop2lem  35245  neibastop2  35246  fgmin  35255  exrecfnlem  36260  heiborlem10  36688  prtlem15  37745  lshpcmp  37858  lsatn0  37869  lsatcmp  37873  lsmsat  37878  lsatcv0  37901  l1cvpat  37924  eqlkr  37969  lshpkrlem1  37980  lshpkrlem6  37985  lfl1dim  37991  lfl1dim2N  37992  lkrss2N  38039  athgt  38327  3dim2  38339  llnle  38389  llncmp  38393  lplnle  38411  lplnnle2at  38412  llncvrlpln2  38428  llncvrlpln  38429  lplncmp  38433  lplnexllnN  38435  lvolnle3at  38453  lplncvrlvol2  38486  lplncvrlvol  38487  lvolcmp  38488  pointpsubN  38622  pclfinN  38771  pclfinclN  38821  osumcllem11N  38837  pexmidlem4N  38844  cdleme17d3  39367  cdlemeg46gfre  39403  cdleme48gfv1  39407  cdleme50trn2  39422  trlord  39440  cdlemg6e  39493  cdlemj3  39694  diaelrnN  39916  diaintclN  39929  dia2dimlem6  39940  cdlemm10N  39989  dibintclN  40038  dihord6apre  40127  dihord5b  40130  dihord5apre  40133  dihglblem5apreN  40162  dihglblem2N  40165  dihglblem3N  40166  dihglbcpreN  40171  dihintcl  40215  lclkrlem2y  40402  lcfrvalsnN  40412  isnacs3  41448  jm2.26  41741  fnwe2lem2  41793  hbtlem5  41870  dflim5  42079  uzwo4  43740  iunincfi  43783  restuni3  43807  disjinfi  43891  ssnnf1octb  43893  choicefi  43899  mapssbi  43912  unirnmapsn  43913  ssmapsn  43915  iunmapsn  43916  supxrgere  44043  supxrgelem  44047  suplesup  44049  infleinf  44082  suplesup2  44086  rexabslelem  44128  islptre  44335  limcperiod  44344  limclner  44367  limsupmnfuzlem  44442  limsupre3lem  44448  coskpi2  44582  cosknegpi  44585  icccncfext  44603  stoweidlem27  44743  stoweidlem59  44775  fourierdlem41  44864  fourierdlem42  44865  fourierdlem70  44892  fourierdlem71  44893  fourierdlem81  44903  fourierswlem  44946  qndenserrnopnlem  45013  subsaliuncl  45074  subsalsal  45075  sge0tsms  45096  sge0fsum  45103  sge0supre  45105  sge0sup  45107  sge0rnbnd  45109  sge0pnffigt  45112  sge0resrn  45120  sge0split  45125  sge0iunmptlemfi  45129  sge0rpcpnf  45137  sge0isum  45143  sge0xaddlem2  45150  sge0uzfsumgt  45160  sge0seq  45162  sge0reuz  45163  nnfoctbdjlem  45171  nnfoctbdj  45172  meadjiunlem  45181  meaiuninclem  45196  carageniuncllem2  45238  caratheodorylem2  45243  ovnsupge0  45273  ovncvrrp  45280  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem2  45318  opnvonmbllem2  45349  ovnovollem3  45374  sssmf  45454  smfpimbor1lem1  45514  smfco  45518  smfpimcc  45524  smfinflem  45533  fmtno4prmfac  46240  sfprmdvdsmersenne  46271  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbnd  46477  imasrng  46678