Theorem rexlimdv 3161

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexlimdva  3163  rexlimdva2  3165  rexlimdv3a  3167  rexlimdvw  3168  rexlimdvv  3218  rexlimdvvva  3220  elpwunsn  4645  onelssex  6407  eldmrexrnb  7085  weniso  7357  ssorduni  7778  onint  7789  limuni3  7848  peano5  7890  funcnvuni  7929  funeldmdif  8045  frxp  8124  smoiun  8350  tfrlem9  8374  oaordex  8545  oalimcl  8547  oaass  8548  findcard2  9159  findcard3  9253  frfi  9255  unblem1  9262  ordiso2  9487  inf3lem3  9609  r1sdom  9756  tz9.12lem3  9771  kardenOLD  9899  infxpenlem  10016  cardinfima  10100  iunfictbso  10117  dfac5  10131  cfcoflem  10274  fin23lem11  10319  fin23lem30  10344  fin1a2lem13  10414  axdc3lem2  10453  konigthlem  10577  fpwwe2lem11  10650  tskuni  10792  axgroth6  10837  nqereu  10938  genpnmax  11016  ltaddpr  11043  recexsrlem  11112  mulgt0sr  11114  axrrecex  11172  axpre-sup  11178  addrid  11414  addlid  11417  recex  11870  btwnz  12724  lbzbi  12985  qbtwnre  13251  caubnd  15446  divalglem9  16491  unbenlem  17000  firest  17517  imasmnd2  18881  imasgrp2  19178  pmtrfrn  19585  pgpfi  19732  sylow2blem3  19749  imasrng  20312  imasring  20471  lspsneq  21309  lspdisj  21312  elcls  23298  elcls3  23308  subbascn  23479  cmpsublem  23624  cmpsub  23625  nllyidm  23715  comppfsc  23758  ptpjopn  23838  fbfinnfr  24067  filin  24080  isfil2  24082  infil  24089  fgss2  24100  fgfil  24101  fgcl  24104  fgabs  24105  elfm2  24174  rnelfm  24179  fmfnfmlem2  24181  fmfnfmlem4  24183  fmco  24187  flffbas  24221  cnpflf2  24226  fclscf  24251  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALTlem4  24276  alexsubALT  24277  neibl  24727  met2ndc  24749  metcnp3  24766  icccmplem2  25050  xrge0tsms  25061  fgcfil  25499  volfiniun  25775  dyadmax  25826  dyadmbllem  25827  c1liplem1  26223  dgrlem  26455  axcontlem10  29430  usgredg2vtxeuALT  29682  ushgredgedg  29689  ushgredgedgloop  29691  uhgrspan1  29763  nbuhgr2vtx1edgblem  29811  erclwwlksym  30491  erclwwlknsym  30540  umgr2cycllem  30625  umgr2cycl  30626  1pthon2v  30633  conngrv2edg  30675  lpni  30961  grpoidinvlem3  30987  grporcan  30999  omlsii  31884  spansncol  32049  spansnss  32052  spanunsni  32060  h1datomi  32062  nmopsetretALT  32344  branmfn  32586  chjatom  32838  cvbr4i  32848  atomli  32863  xrge0tsmsd  33513  sat1el2xp  35958  fmlasuc  35965  satffunlem1lem2  35982  satffunlem2lem1  35983  satffunlem2lem2  35985  dfon2lem6  36365  colineardim1  36641  finminlem  36937  nn0prpwlem  36941  neibastop2lem  36979  neibastop2  36980  fgmin  36989  exrecfnlem  38133  heiborlem10  38570  prtlem15  39748  lshpcmp  39861  lsatn0  39872  lsatcmp  39876  lsmsat  39881  lsatcv0  39904  l1cvpat  39927  eqlkr  39972  lshpkrlem1  39983  lshpkrlem6  39988  lfl1dim  39994  lfl1dim2N  39995  lkrss2N  40042  athgt  40329  3dim2  40341  llnle  40391  llncmp  40395  lplnle  40413  lplnnle2at  40414  llncvrlpln2  40430  llncvrlpln  40431  lplncmp  40435  lplnexllnN  40437  lvolnle3at  40455  lplncvrlvol2  40488  lplncvrlvol  40489  lvolcmp  40490  pointpsubN  40624  pclfinN  40773  pclfinclN  40823  osumcllem11N  40839  pexmidlem4N  40846  cdleme17d3  41369  cdlemeg46gfre  41405  cdleme48gfv1  41409  cdleme50trn2  41424  trlord  41442  cdlemg6e  41495  cdlemj3  41696  diaelrnN  41918  diaintclN  41931  dia2dimlem6  41942  cdlemm10N  41991  dibintclN  42040  dihord6apre  42129  dihord5b  42132  dihord5apre  42135  dihglblem5apreN  42164  dihglblem2N  42167  dihglblem3N  42168  dihglbcpreN  42173  dihintcl  42217  lclkrlem2y  42404  lcfrvalsnN  42414  isnacs3  43555  jm2.26  43843  fnwe2lem2  43892  hbtlem5  43969  dflim5  44170  uzwo4  45887  iunincfi  45926  restuni3  45950  disjinfi  46024  ssnnf1octb  46026  choicefi  46031  mapssbi  46043  unirnmapsn  46044  iunmapsn  46047  supxrgere  46163  supxrgelem  46167  suplesup  46169  infleinf  46201  suplesup2  46205  rexabslelem  46246  islptre  46449  limcperiod  46458  limclner  46479  limsupmnfuzlem  46554  limsupre3lem  46560  coskpi2  46694  cosknegpi  46697  icccncfext  46715  stoweidlem27  46855  stoweidlem59  46887  fourierdlem41  46976  fourierdlem42  46977  fourierdlem70  47004  fourierdlem71  47005  fourierdlem81  47015  fourierswlem  47058  qndenserrnopnlem  47125  subsaliuncl  47186  subsalsal  47187  sge0tsms  47208  sge0fsum  47215  sge0supre  47217  sge0sup  47219  sge0rnbnd  47221  sge0pnffigt  47224  sge0resrn  47232  sge0split  47237  sge0iunmptlemfi  47241  sge0rpcpnf  47249  sge0isum  47255  sge0xaddlem2  47262  sge0uzfsumgt  47272  sge0seq  47274  sge0reuz  47275  nnfoctbdjlem  47283  nnfoctbdj  47284  meadjiunlem  47293  meaiuninclem  47308  carageniuncllem2  47350  caratheodorylem2  47355  ovnsupge0  47385  ovncvrrp  47392  hoidmv1lelem3  47421  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  ovnhoilem2  47430  opnvonmbllem2  47461  ovnovollem3  47486  smfpimbor1lem1  47626  smfco  47630  smfpimcc  47636  smfinflem  47645  nprmmul3  48429  fmtno4prmfac  48475  sfprmdvdsmersenne  48506  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbnd  48725  grimuhgr  48803  clnbgrgrim  48850  uspgrlimlem2  48905