Theorem rexlimdv 3135

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3060

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 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  rexlimdva  3137  rexlimdva2  3139  rexlimdv3a  3141  rexlimdvw  3142  rexlimdvv  3192  rexlimdvvva  3194  elpwunsn  4641  onelssex  6366  eldmrexrnb  7037  weniso  7300  ssorduni  7724  onint  7735  limuni3  7794  peano5  7835  funcnvuni  7874  funeldmdif  7992  frxp  8068  smoiun  8293  tfrlem9  8316  oaordex  8485  oalimcl  8487  oaass  8488  findcard2  9089  findcard3  9183  frfi  9185  unblem1  9192  ordiso2  9420  inf3lem3  9539  r1sdom  9686  tz9.12lem3  9701  karden  9807  infxpenlem  9923  cardinfima  10007  iunfictbso  10024  dfac5  10039  cfcoflem  10182  fin23lem11  10227  fin23lem30  10252  fin1a2lem13  10322  axdc3lem2  10361  konigthlem  10479  fpwwe2lem11  10552  tskuni  10694  axgroth6  10739  nqereu  10840  genpnmax  10918  ltaddpr  10945  recexsrlem  11014  mulgt0sr  11016  axrrecex  11074  axpre-sup  11080  addrid  11313  addlid  11316  recex  11769  btwnz  12595  lbzbi  12849  qbtwnre  13114  caubnd  15282  divalglem9  16328  unbenlem  16836  firest  17352  imasmnd2  18699  imasgrp2  18985  pmtrfrn  19387  pgpfi  19534  sylow2blem3  19551  imasrng  20112  imasring  20266  lspsneq  21077  lspdisj  21080  elcls  23017  elcls3  23027  subbascn  23198  cmpsublem  23343  cmpsub  23344  nllyidm  23433  comppfsc  23476  ptpjopn  23556  fbfinnfr  23785  filin  23798  isfil2  23800  infil  23807  fgss2  23818  fgfil  23819  fgcl  23822  fgabs  23823  elfm2  23892  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fmco  23905  flffbas  23939  cnpflf2  23944  fclscf  23969  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  neibl  24445  met2ndc  24467  metcnp3  24484  icccmplem2  24768  xrge0tsms  24779  fgcfil  25227  volfiniun  25504  dyadmax  25555  dyadmbllem  25556  c1liplem1  25957  dgrlem  26190  axcontlem10  29046  usgredg2vtxeuALT  29295  ushgredgedg  29302  ushgredgedgloop  29304  uhgrspan1  29376  nbuhgr2vtx1edgblem  29424  erclwwlksym  30096  erclwwlknsym  30145  1pthon2v  30228  conngrv2edg  30270  lpni  30555  grpoidinvlem3  30581  grporcan  30593  omlsii  31478  spansncol  31643  spansnss  31646  spanunsni  31654  h1datomi  31656  nmopsetretALT  31938  branmfn  32180  chjatom  32432  cvbr4i  32442  atomli  32457  xrge0tsmsd  33155  umgr2cycllem  35334  umgr2cycl  35335  sat1el2xp  35573  fmlasuc  35580  satffunlem1lem2  35597  satffunlem2lem1  35598  satffunlem2lem2  35600  dfon2lem6  35980  colineardim1  36255  finminlem  36512  nn0prpwlem  36516  neibastop2lem  36554  neibastop2  36555  fgmin  36564  exrecfnlem  37584  heiborlem10  38021  prtlem15  39135  lshpcmp  39248  lsatn0  39259  lsatcmp  39263  lsmsat  39268  lsatcv0  39291  l1cvpat  39314  eqlkr  39359  lshpkrlem1  39370  lshpkrlem6  39375  lfl1dim  39381  lfl1dim2N  39382  lkrss2N  39429  athgt  39716  3dim2  39728  llnle  39778  llncmp  39782  lplnle  39800  lplnnle2at  39801  llncvrlpln2  39817  llncvrlpln  39818  lplncmp  39822  lplnexllnN  39824  lvolnle3at  39842  lplncvrlvol2  39875  lplncvrlvol  39876  lvolcmp  39877  pointpsubN  40011  pclfinN  40160  pclfinclN  40210  osumcllem11N  40226  pexmidlem4N  40233  cdleme17d3  40756  cdlemeg46gfre  40792  cdleme48gfv1  40796  cdleme50trn2  40811  trlord  40829  cdlemg6e  40882  cdlemj3  41083  diaelrnN  41305  diaintclN  41318  dia2dimlem6  41329  cdlemm10N  41378  dibintclN  41427  dihord6apre  41516  dihord5b  41519  dihord5apre  41522  dihglblem5apreN  41551  dihglblem2N  41554  dihglblem3N  41555  dihglbcpreN  41560  dihintcl  41604  lclkrlem2y  41791  lcfrvalsnN  41801  isnacs3  42952  jm2.26  43244  fnwe2lem2  43293  hbtlem5  43370  dflim5  43571  uzwo4  45298  iunincfi  45338  restuni3  45362  disjinfi  45436  ssnnf1octb  45438  choicefi  45444  mapssbi  45457  unirnmapsn  45458  iunmapsn  45461  supxrgere  45578  supxrgelem  45582  suplesup  45584  infleinf  45616  suplesup2  45620  rexabslelem  45662  islptre  45865  limcperiod  45874  limclner  45895  limsupmnfuzlem  45970  limsupre3lem  45976  coskpi2  46110  cosknegpi  46113  icccncfext  46131  stoweidlem27  46271  stoweidlem59  46303  fourierdlem41  46392  fourierdlem42  46393  fourierdlem70  46420  fourierdlem71  46421  fourierdlem81  46431  fourierswlem  46474  qndenserrnopnlem  46541  subsaliuncl  46602  subsalsal  46603  sge0tsms  46624  sge0fsum  46631  sge0supre  46633  sge0sup  46635  sge0rnbnd  46637  sge0pnffigt  46640  sge0resrn  46648  sge0split  46653  sge0iunmptlemfi  46657  sge0rpcpnf  46665  sge0isum  46671  sge0xaddlem2  46678  sge0uzfsumgt  46688  sge0seq  46690  sge0reuz  46691  nnfoctbdjlem  46699  nnfoctbdj  46700  meadjiunlem  46709  meaiuninclem  46724  carageniuncllem2  46766  caratheodorylem2  46771  ovnsupge0  46801  ovncvrrp  46808  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  ovnhoilem2  46846  opnvonmbllem2  46877  ovnovollem3  46902  sssmf  46982  smfpimbor1lem1  47042  smfco  47046  smfpimcc  47052  smfinflem  47061  fmtno4prmfac  47818  sfprmdvdsmersenne  47849  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbnd  48055  grimuhgr  48133  clnbgrgrim  48180  uspgrlimlem2  48235