Theorem rexlimdv 3166

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091

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 3092

This theorem is used by:  rexlimdva  3168  rexlimdva2  3170  rexlimdv3a  3172  rexlimdvw  3173  rexlimdvv  3223  rexlimdvvva  3225  elpwunsn  4652  onelssex  6414  eldmrexrnb  7091  weniso  7360  ssorduni  7780  onint  7791  limuni3  7850  peano5  7892  funcnvuni  7931  funeldmdif  8047  frxp  8124  smoiun  8350  tfrlem9  8374  oaordex  8545  oalimcl  8547  oaass  8548  findcard2  9152  findcard3  9246  frfi  9248  unblem1  9255  ordiso2  9480  inf3lem3  9602  r1sdom  9749  tz9.12lem3  9764  kardenOLD  9892  infxpenlem  10009  cardinfima  10093  iunfictbso  10110  dfac5  10124  cfcoflem  10267  fin23lem11  10312  fin23lem30  10337  fin1a2lem13  10407  axdc3lem2  10446  konigthlem  10564  fpwwe2lem11  10637  tskuni  10779  axgroth6  10824  nqereu  10925  genpnmax  11003  ltaddpr  11030  recexsrlem  11099  mulgt0sr  11101  axrrecex  11159  axpre-sup  11165  addrid  11401  addlid  11404  recex  11857  btwnz  12710  lbzbi  12971  qbtwnre  13236  caubnd  15429  divalglem9  16476  unbenlem  16985  firest  17502  imasmnd2  18855  imasgrp2  19144  pmtrfrn  19551  pgpfi  19698  sylow2blem3  19715  imasrng  20278  imasring  20437  lspsneq  21275  lspdisj  21278  elcls  23259  elcls3  23269  subbascn  23440  cmpsublem  23585  cmpsub  23586  nllyidm  23675  comppfsc  23718  ptpjopn  23798  fbfinnfr  24027  filin  24040  isfil2  24042  infil  24049  fgss2  24060  fgfil  24061  fgcl  24064  fgabs  24065  elfm2  24134  rnelfm  24139  fmfnfmlem2  24141  fmfnfmlem4  24143  fmco  24147  flffbas  24181  cnpflf2  24186  fclscf  24211  alexsubALTlem2  24234  alexsubALTlem3  24235  alexsubALTlem4  24236  alexsubALT  24237  neibl  24687  met2ndc  24709  metcnp3  24726  icccmplem2  25010  xrge0tsms  25021  fgcfil  25459  volfiniun  25735  dyadmax  25786  dyadmbllem  25787  c1liplem1  26184  dgrlem  26415  axcontlem10  29352  usgredg2vtxeuALT  29601  ushgredgedg  29608  ushgredgedgloop  29610  uhgrspan1  29682  nbuhgr2vtx1edgblem  29730  erclwwlksym  30401  erclwwlknsym  30450  1pthon2v  30533  conngrv2edg  30575  lpni  30861  grpoidinvlem3  30887  grporcan  30899  omlsii  31784  spansncol  31949  spansnss  31952  spanunsni  31960  h1datomi  31962  nmopsetretALT  32244  branmfn  32486  chjatom  32738  cvbr4i  32748  atomli  32763  xrge0tsmsd  33416  umgr2cycllem  35645  umgr2cycl  35646  sat1el2xp  35884  fmlasuc  35891  satffunlem1lem2  35908  satffunlem2lem1  35909  satffunlem2lem2  35911  dfon2lem6  36291  colineardim1  36566  finminlem  36862  nn0prpwlem  36866  neibastop2lem  36904  neibastop2  36905  fgmin  36914  exrecfnlem  38058  heiborlem10  38504  prtlem15  39682  lshpcmp  39795  lsatn0  39806  lsatcmp  39810  lsmsat  39815  lsatcv0  39838  l1cvpat  39861  eqlkr  39906  lshpkrlem1  39917  lshpkrlem6  39922  lfl1dim  39928  lfl1dim2N  39929  lkrss2N  39976  athgt  40263  3dim2  40275  llnle  40325  llncmp  40329  lplnle  40347  lplnnle2at  40348  llncvrlpln2  40364  llncvrlpln  40365  lplncmp  40369  lplnexllnN  40371  lvolnle3at  40389  lplncvrlvol2  40422  lplncvrlvol  40423  lvolcmp  40424  pointpsubN  40558  pclfinN  40707  pclfinclN  40757  osumcllem11N  40773  pexmidlem4N  40780  cdleme17d3  41303  cdlemeg46gfre  41339  cdleme48gfv1  41343  cdleme50trn2  41358  trlord  41376  cdlemg6e  41429  cdlemj3  41630  diaelrnN  41852  diaintclN  41865  dia2dimlem6  41876  cdlemm10N  41925  dibintclN  41974  dihord6apre  42063  dihord5b  42066  dihord5apre  42069  dihglblem5apreN  42098  dihglblem2N  42101  dihglblem3N  42102  dihglbcpreN  42107  dihintcl  42151  lclkrlem2y  42338  lcfrvalsnN  42348  isnacs3  43474  jm2.26  43762  fnwe2lem2  43811  hbtlem5  43888  dflim5  44089  uzwo4  45806  iunincfi  45845  restuni3  45869  disjinfi  45943  ssnnf1octb  45945  choicefi  45950  mapssbi  45962  unirnmapsn  45963  iunmapsn  45966  supxrgere  46082  supxrgelem  46086  suplesup  46088  infleinf  46120  suplesup2  46124  rexabslelem  46165  islptre  46368  limcperiod  46377  limclner  46398  limsupmnfuzlem  46473  limsupre3lem  46479  coskpi2  46613  cosknegpi  46616  icccncfext  46634  stoweidlem27  46774  stoweidlem59  46806  fourierdlem41  46895  fourierdlem42  46896  fourierdlem70  46923  fourierdlem71  46924  fourierdlem81  46934  fourierswlem  46977  qndenserrnopnlem  47044  subsaliuncl  47105  subsalsal  47106  sge0tsms  47127  sge0fsum  47134  sge0supre  47136  sge0sup  47138  sge0rnbnd  47140  sge0pnffigt  47143  sge0resrn  47151  sge0split  47156  sge0iunmptlemfi  47160  sge0rpcpnf  47168  sge0isum  47174  sge0xaddlem2  47181  sge0uzfsumgt  47191  sge0seq  47193  sge0reuz  47194  nnfoctbdjlem  47202  nnfoctbdj  47203  meadjiunlem  47212  meaiuninclem  47227  carageniuncllem2  47269  caratheodorylem2  47274  ovnsupge0  47304  ovncvrrp  47311  hoidmv1lelem3  47340  hoidmv1le  47341  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem3  47344  ovnhoilem2  47349  opnvonmbllem2  47380  ovnovollem3  47405  smfpimbor1lem1  47545  smfco  47549  smfpimcc  47555  smfinflem  47564  nprmmul3  48311  fmtno4prmfac  48357  sfprmdvdsmersenne  48388  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbtbnd  48607  grimuhgr  48685  clnbgrgrim  48732  uspgrlimlem2  48787