Theorem rexlimdv 3139

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimdva  3141  rexlimdva2  3143  rexlimdv3a  3145  rexlimdvw  3146  rexlimdvv  3196  rexlimdvvva  3198  elpwunsn  4623  onelssex  6366  eldmrexrnb  7040  weniso  7305  ssorduni  7729  onint  7740  limuni3  7799  peano5  7840  funcnvuni  7879  funeldmdif  7997  frxp  8073  smoiun  8298  tfrlem9  8321  oaordex  8490  oalimcl  8492  oaass  8493  findcard2  9096  findcard3  9190  frfi  9192  unblem1  9199  ordiso2  9427  inf3lem3  9549  r1sdom  9696  tz9.12lem3  9711  karden  9817  infxpenlem  9933  cardinfima  10017  iunfictbso  10034  dfac5  10049  cfcoflem  10192  fin23lem11  10237  fin23lem30  10262  fin1a2lem13  10332  axdc3lem2  10371  konigthlem  10489  fpwwe2lem11  10562  tskuni  10704  axgroth6  10749  nqereu  10850  genpnmax  10928  ltaddpr  10955  recexsrlem  11024  mulgt0sr  11026  axrrecex  11084  axpre-sup  11090  addrid  11324  addlid  11327  recex  11780  btwnz  12630  lbzbi  12884  qbtwnre  13149  caubnd  15319  divalglem9  16368  unbenlem  16877  firest  17393  imasmnd2  18740  imasgrp2  19029  pmtrfrn  19431  pgpfi  19578  sylow2blem3  19595  imasrng  20156  imasring  20308  lspsneq  21122  lspdisj  21125  elcls  23063  elcls3  23073  subbascn  23244  cmpsublem  23389  cmpsub  23390  nllyidm  23479  comppfsc  23522  ptpjopn  23602  fbfinnfr  23831  filin  23844  isfil2  23846  infil  23853  fgss2  23864  fgfil  23865  fgcl  23868  fgabs  23869  elfm2  23938  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  fmco  23951  flffbas  23985  cnpflf2  23990  fclscf  24015  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  alexsubALT  24041  neibl  24491  met2ndc  24513  metcnp3  24530  icccmplem2  24814  xrge0tsms  24825  fgcfil  25263  volfiniun  25539  dyadmax  25590  dyadmbllem  25591  c1liplem1  25988  dgrlem  26219  axcontlem10  29067  usgredg2vtxeuALT  29316  ushgredgedg  29323  ushgredgedgloop  29325  uhgrspan1  29397  nbuhgr2vtx1edgblem  29445  erclwwlksym  30116  erclwwlknsym  30165  1pthon2v  30248  conngrv2edg  30290  lpni  30576  grpoidinvlem3  30602  grporcan  30614  omlsii  31499  spansncol  31664  spansnss  31667  spanunsni  31675  h1datomi  31677  nmopsetretALT  31959  branmfn  32201  chjatom  32453  cvbr4i  32463  atomli  32478  xrge0tsmsd  33161  umgr2cycllem  35375  umgr2cycl  35376  sat1el2xp  35614  fmlasuc  35621  satffunlem1lem2  35638  satffunlem2lem1  35639  satffunlem2lem2  35641  dfon2lem6  36021  colineardim1  36296  finminlem  36553  nn0prpwlem  36557  neibastop2lem  36595  neibastop2  36596  fgmin  36605  exrecfnlem  37748  heiborlem10  38194  prtlem15  39374  lshpcmp  39487  lsatn0  39498  lsatcmp  39502  lsmsat  39507  lsatcv0  39530  l1cvpat  39553  eqlkr  39598  lshpkrlem1  39609  lshpkrlem6  39614  lfl1dim  39620  lfl1dim2N  39621  lkrss2N  39668  athgt  39955  3dim2  39967  llnle  40017  llncmp  40021  lplnle  40039  lplnnle2at  40040  llncvrlpln2  40056  llncvrlpln  40057  lplncmp  40061  lplnexllnN  40063  lvolnle3at  40081  lplncvrlvol2  40114  lplncvrlvol  40115  lvolcmp  40116  pointpsubN  40250  pclfinN  40399  pclfinclN  40449  osumcllem11N  40465  pexmidlem4N  40472  cdleme17d3  40995  cdlemeg46gfre  41031  cdleme48gfv1  41035  cdleme50trn2  41050  trlord  41068  cdlemg6e  41121  cdlemj3  41322  diaelrnN  41544  diaintclN  41557  dia2dimlem6  41568  cdlemm10N  41617  dibintclN  41666  dihord6apre  41755  dihord5b  41758  dihord5apre  41761  dihglblem5apreN  41790  dihglblem2N  41793  dihglblem3N  41794  dihglbcpreN  41799  dihintcl  41843  lclkrlem2y  42030  lcfrvalsnN  42040  isnacs3  43166  jm2.26  43454  fnwe2lem2  43503  hbtlem5  43580  dflim5  43781  uzwo4  45508  iunincfi  45548  restuni3  45572  disjinfi  45646  ssnnf1octb  45648  choicefi  45653  mapssbi  45665  unirnmapsn  45666  iunmapsn  45669  supxrgere  45785  supxrgelem  45789  suplesup  45791  infleinf  45823  suplesup2  45827  rexabslelem  45868  islptre  46071  limcperiod  46080  limclner  46101  limsupmnfuzlem  46176  limsupre3lem  46182  coskpi2  46316  cosknegpi  46319  icccncfext  46337  stoweidlem27  46477  stoweidlem59  46509  fourierdlem41  46598  fourierdlem42  46599  fourierdlem70  46626  fourierdlem71  46627  fourierdlem81  46637  fourierswlem  46680  qndenserrnopnlem  46747  subsaliuncl  46808  subsalsal  46809  sge0tsms  46830  sge0fsum  46837  sge0supre  46839  sge0sup  46841  sge0rnbnd  46843  sge0pnffigt  46846  sge0resrn  46854  sge0split  46859  sge0iunmptlemfi  46863  sge0rpcpnf  46871  sge0isum  46877  sge0xaddlem2  46884  sge0uzfsumgt  46894  sge0seq  46896  sge0reuz  46897  nnfoctbdjlem  46905  nnfoctbdj  46906  meadjiunlem  46915  meaiuninclem  46930  carageniuncllem2  46972  caratheodorylem2  46977  ovnsupge0  47007  ovncvrrp  47014  hoidmv1lelem3  47043  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem2  47052  opnvonmbllem2  47083  ovnovollem3  47108  sssmf  47188  smfpimbor1lem1  47248  smfco  47252  smfpimcc  47258  smfinflem  47267  nprmmul3  48011  fmtno4prmfac  48057  sfprmdvdsmersenne  48088  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbtbnd  48307  grimuhgr  48385  clnbgrgrim  48432  uspgrlimlem2  48487