Theorem rexlimdv 3137

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimdva  3139  rexlimdva2  3141  rexlimdv3a  3143  rexlimdvw  3144  rexlimdvv  3194  rexlimdvvva  3196  elpwunsn  4629  onelssex  6366  eldmrexrnb  7038  weniso  7302  ssorduni  7726  onint  7737  limuni3  7796  peano5  7837  funcnvuni  7876  funeldmdif  7994  frxp  8069  smoiun  8294  tfrlem9  8317  oaordex  8486  oalimcl  8488  oaass  8489  findcard2  9092  findcard3  9186  frfi  9188  unblem1  9195  ordiso2  9423  inf3lem3  9542  r1sdom  9689  tz9.12lem3  9704  karden  9810  infxpenlem  9926  cardinfima  10010  iunfictbso  10027  dfac5  10042  cfcoflem  10185  fin23lem11  10230  fin23lem30  10255  fin1a2lem13  10325  axdc3lem2  10364  konigthlem  10482  fpwwe2lem11  10555  tskuni  10697  axgroth6  10742  nqereu  10843  genpnmax  10921  ltaddpr  10948  recexsrlem  11017  mulgt0sr  11019  axrrecex  11077  axpre-sup  11083  addrid  11317  addlid  11320  recex  11773  btwnz  12623  lbzbi  12877  qbtwnre  13142  caubnd  15312  divalglem9  16361  unbenlem  16870  firest  17386  imasmnd2  18733  imasgrp2  19022  pmtrfrn  19424  pgpfi  19571  sylow2blem3  19588  imasrng  20149  imasring  20301  lspsneq  21112  lspdisj  21115  elcls  23048  elcls3  23058  subbascn  23229  cmpsublem  23374  cmpsub  23375  nllyidm  23464  comppfsc  23507  ptpjopn  23587  fbfinnfr  23816  filin  23829  isfil2  23831  infil  23838  fgss2  23849  fgfil  23850  fgcl  23853  fgabs  23854  elfm2  23923  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  fmco  23936  flffbas  23970  cnpflf2  23975  fclscf  24000  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  neibl  24476  met2ndc  24498  metcnp3  24515  icccmplem2  24799  xrge0tsms  24810  fgcfil  25248  volfiniun  25524  dyadmax  25575  dyadmbllem  25576  c1liplem1  25973  dgrlem  26204  axcontlem10  29056  usgredg2vtxeuALT  29305  ushgredgedg  29312  ushgredgedgloop  29314  uhgrspan1  29386  nbuhgr2vtx1edgblem  29434  erclwwlksym  30106  erclwwlknsym  30155  1pthon2v  30238  conngrv2edg  30280  lpni  30566  grpoidinvlem3  30592  grporcan  30604  omlsii  31489  spansncol  31654  spansnss  31657  spanunsni  31665  h1datomi  31667  nmopsetretALT  31949  branmfn  32191  chjatom  32443  cvbr4i  32453  atomli  32468  xrge0tsmsd  33149  umgr2cycllem  35338  umgr2cycl  35339  sat1el2xp  35577  fmlasuc  35584  satffunlem1lem2  35601  satffunlem2lem1  35602  satffunlem2lem2  35604  dfon2lem6  35984  colineardim1  36259  finminlem  36516  nn0prpwlem  36520  neibastop2lem  36558  neibastop2  36559  fgmin  36568  exrecfnlem  37709  heiborlem10  38155  prtlem15  39335  lshpcmp  39448  lsatn0  39459  lsatcmp  39463  lsmsat  39468  lsatcv0  39491  l1cvpat  39514  eqlkr  39559  lshpkrlem1  39570  lshpkrlem6  39575  lfl1dim  39581  lfl1dim2N  39582  lkrss2N  39629  athgt  39916  3dim2  39928  llnle  39978  llncmp  39982  lplnle  40000  lplnnle2at  40001  llncvrlpln2  40017  llncvrlpln  40018  lplncmp  40022  lplnexllnN  40024  lvolnle3at  40042  lplncvrlvol2  40075  lplncvrlvol  40076  lvolcmp  40077  pointpsubN  40211  pclfinN  40360  pclfinclN  40410  osumcllem11N  40426  pexmidlem4N  40433  cdleme17d3  40956  cdlemeg46gfre  40992  cdleme48gfv1  40996  cdleme50trn2  41011  trlord  41029  cdlemg6e  41082  cdlemj3  41283  diaelrnN  41505  diaintclN  41518  dia2dimlem6  41529  cdlemm10N  41578  dibintclN  41627  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dihglblem5apreN  41751  dihglblem2N  41754  dihglblem3N  41755  dihglbcpreN  41760  dihintcl  41804  lclkrlem2y  41991  lcfrvalsnN  42001  isnacs3  43156  jm2.26  43448  fnwe2lem2  43497  hbtlem5  43574  dflim5  43775  uzwo4  45502  iunincfi  45542  restuni3  45566  disjinfi  45640  ssnnf1octb  45642  choicefi  45647  mapssbi  45660  unirnmapsn  45661  iunmapsn  45664  supxrgere  45781  supxrgelem  45785  suplesup  45787  infleinf  45819  suplesup2  45823  rexabslelem  45864  islptre  46067  limcperiod  46076  limclner  46097  limsupmnfuzlem  46172  limsupre3lem  46178  coskpi2  46312  cosknegpi  46315  icccncfext  46333  stoweidlem27  46473  stoweidlem59  46505  fourierdlem41  46594  fourierdlem42  46595  fourierdlem70  46622  fourierdlem71  46623  fourierdlem81  46633  fourierswlem  46676  qndenserrnopnlem  46743  subsaliuncl  46804  subsalsal  46805  sge0tsms  46826  sge0fsum  46833  sge0supre  46835  sge0sup  46837  sge0rnbnd  46839  sge0pnffigt  46842  sge0resrn  46850  sge0split  46855  sge0iunmptlemfi  46859  sge0rpcpnf  46867  sge0isum  46873  sge0xaddlem2  46880  sge0uzfsumgt  46890  sge0seq  46892  sge0reuz  46893  nnfoctbdjlem  46901  nnfoctbdj  46902  meadjiunlem  46911  meaiuninclem  46926  carageniuncllem2  46968  caratheodorylem2  46973  ovnsupge0  47003  ovncvrrp  47010  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoilem2  47048  opnvonmbllem2  47079  ovnovollem3  47104  sssmf  47184  smfpimbor1lem1  47244  smfco  47248  smfpimcc  47254  smfinflem  47263  nprmmul3  48001  fmtno4prmfac  48047  sfprmdvdsmersenne  48078  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbnd  48297  grimuhgr  48375  clnbgrgrim  48422  uspgrlimlem2  48477