Theorem rexlimdv 3164

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimdva  3166  rexlimdva2  3168  rexlimdv3a  3170  rexlimdvw  3171  rexlimdvv  3221  rexlimdvvva  3223  elpwunsn  4651  onelssex  6412  eldmrexrnb  7089  weniso  7354  ssorduni  7779  onint  7790  limuni3  7849  peano5  7891  funcnvuni  7930  funeldmdif  8046  frxp  8123  smoiun  8349  tfrlem9  8373  oaordex  8544  oalimcl  8546  oaass  8547  findcard2  9150  findcard3  9244  frfi  9246  unblem1  9253  ordiso2  9478  inf3lem3  9600  r1sdom  9747  tz9.12lem3  9762  karden  9882  infxpenlem  9998  cardinfima  10082  iunfictbso  10099  dfac5  10113  cfcoflem  10257  fin23lem11  10302  fin23lem30  10327  fin1a2lem13  10397  axdc3lem2  10436  konigthlem  10554  fpwwe2lem11  10627  tskuni  10769  axgroth6  10814  nqereu  10915  genpnmax  10993  ltaddpr  11020  recexsrlem  11089  mulgt0sr  11091  axrrecex  11149  axpre-sup  11155  addrid  11391  addlid  11394  recex  11847  btwnz  12700  lbzbi  12961  qbtwnre  13226  caubnd  15412  divalglem9  16460  unbenlem  16969  firest  17486  imasmnd2  18833  imasgrp2  19122  pmtrfrn  19529  pgpfi  19676  sylow2blem3  19693  imasrng  20256  imasring  20413  lspsneq  21227  lspdisj  21230  elcls  23211  elcls3  23221  subbascn  23392  cmpsublem  23537  cmpsub  23538  nllyidm  23627  comppfsc  23670  ptpjopn  23750  fbfinnfr  23979  filin  23992  isfil2  23994  infil  24001  fgss2  24012  fgfil  24013  fgcl  24016  fgabs  24017  elfm2  24086  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  fmco  24099  flffbas  24133  cnpflf2  24138  fclscf  24163  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  alexsubALT  24189  neibl  24639  met2ndc  24661  metcnp3  24678  icccmplem2  24962  xrge0tsms  24973  fgcfil  25411  volfiniun  25687  dyadmax  25738  dyadmbllem  25739  c1liplem1  26136  dgrlem  26367  axcontlem10  29304  usgredg2vtxeuALT  29553  ushgredgedg  29560  ushgredgedgloop  29562  uhgrspan1  29634  nbuhgr2vtx1edgblem  29682  erclwwlksym  30353  erclwwlknsym  30402  1pthon2v  30485  conngrv2edg  30527  lpni  30813  grpoidinvlem3  30839  grporcan  30851  omlsii  31736  spansncol  31901  spansnss  31904  spanunsni  31912  h1datomi  31914  nmopsetretALT  32196  branmfn  32438  chjatom  32690  cvbr4i  32700  atomli  32715  xrge0tsmsd  33374  umgr2cycllem  35613  umgr2cycl  35614  sat1el2xp  35852  fmlasuc  35859  satffunlem1lem2  35876  satffunlem2lem1  35877  satffunlem2lem2  35879  dfon2lem6  36259  colineardim1  36534  finminlem  36810  nn0prpwlem  36814  neibastop2lem  36852  neibastop2  36853  fgmin  36862  exrecfnlem  38006  heiborlem10  38452  prtlem15  39630  lshpcmp  39743  lsatn0  39754  lsatcmp  39758  lsmsat  39763  lsatcv0  39786  l1cvpat  39809  eqlkr  39854  lshpkrlem1  39865  lshpkrlem6  39870  lfl1dim  39876  lfl1dim2N  39877  lkrss2N  39924  athgt  40211  3dim2  40223  llnle  40273  llncmp  40277  lplnle  40295  lplnnle2at  40296  llncvrlpln2  40312  llncvrlpln  40313  lplncmp  40317  lplnexllnN  40319  lvolnle3at  40337  lplncvrlvol2  40370  lplncvrlvol  40371  lvolcmp  40372  pointpsubN  40506  pclfinN  40655  pclfinclN  40705  osumcllem11N  40721  pexmidlem4N  40728  cdleme17d3  41251  cdlemeg46gfre  41287  cdleme48gfv1  41291  cdleme50trn2  41306  trlord  41324  cdlemg6e  41377  cdlemj3  41578  diaelrnN  41800  diaintclN  41813  dia2dimlem6  41824  cdlemm10N  41873  dibintclN  41922  dihord6apre  42011  dihord5b  42014  dihord5apre  42017  dihglblem5apreN  42046  dihglblem2N  42049  dihglblem3N  42050  dihglbcpreN  42055  dihintcl  42099  lclkrlem2y  42286  lcfrvalsnN  42296  isnacs3  43424  jm2.26  43712  fnwe2lem2  43761  hbtlem5  43838  dflim5  44039  uzwo4  45756  iunincfi  45795  restuni3  45819  disjinfi  45893  ssnnf1octb  45895  choicefi  45900  mapssbi  45912  unirnmapsn  45913  iunmapsn  45916  supxrgere  46032  supxrgelem  46036  suplesup  46038  infleinf  46070  suplesup2  46074  rexabslelem  46115  islptre  46318  limcperiod  46327  limclner  46348  limsupmnfuzlem  46423  limsupre3lem  46429  coskpi2  46563  cosknegpi  46566  icccncfext  46584  stoweidlem27  46724  stoweidlem59  46756  fourierdlem41  46845  fourierdlem42  46846  fourierdlem70  46873  fourierdlem71  46874  fourierdlem81  46884  fourierswlem  46927  qndenserrnopnlem  46994  subsaliuncl  47055  subsalsal  47056  sge0tsms  47077  sge0fsum  47084  sge0supre  47086  sge0sup  47088  sge0rnbnd  47090  sge0pnffigt  47093  sge0resrn  47101  sge0split  47106  sge0iunmptlemfi  47110  sge0rpcpnf  47118  sge0isum  47124  sge0xaddlem2  47131  sge0uzfsumgt  47141  sge0seq  47143  sge0reuz  47144  nnfoctbdjlem  47152  nnfoctbdj  47153  meadjiunlem  47162  meaiuninclem  47177  carageniuncllem2  47219  caratheodorylem2  47224  ovnsupge0  47254  ovncvrrp  47261  hoidmv1lelem3  47290  hoidmv1le  47291  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  ovnhoilem2  47299  opnvonmbllem2  47330  ovnovollem3  47355  smfpimbor1lem1  47495  smfco  47499  smfpimcc  47505  smfinflem  47514  nprmmul3  48261  fmtno4prmfac  48307  sfprmdvdsmersenne  48338  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  bgoldbtbnd  48557  grimuhgr  48635  clnbgrgrim  48682  uspgrlimlem2  48737