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  4643  onelssex  6374  eldmrexrnb  7046  weniso  7310  ssorduni  7734  onint  7745  limuni3  7804  peano5  7845  funcnvuni  7884  funeldmdif  8002  frxp  8078  smoiun  8303  tfrlem9  8326  oaordex  8495  oalimcl  8497  oaass  8498  findcard2  9101  findcard3  9195  frfi  9197  unblem1  9204  ordiso2  9432  inf3lem3  9551  r1sdom  9698  tz9.12lem3  9713  karden  9819  infxpenlem  9935  cardinfima  10019  iunfictbso  10036  dfac5  10051  cfcoflem  10194  fin23lem11  10239  fin23lem30  10264  fin1a2lem13  10334  axdc3lem2  10373  konigthlem  10491  fpwwe2lem11  10564  tskuni  10706  axgroth6  10751  nqereu  10852  genpnmax  10930  ltaddpr  10957  recexsrlem  11026  mulgt0sr  11028  axrrecex  11086  axpre-sup  11092  addrid  11325  addlid  11328  recex  11781  btwnz  12607  lbzbi  12861  qbtwnre  13126  caubnd  15294  divalglem9  16340  unbenlem  16848  firest  17364  imasmnd2  18711  imasgrp2  18997  pmtrfrn  19399  pgpfi  19546  sylow2blem3  19563  imasrng  20124  imasring  20278  lspsneq  21089  lspdisj  21092  elcls  23029  elcls3  23039  subbascn  23210  cmpsublem  23355  cmpsub  23356  nllyidm  23445  comppfsc  23488  ptpjopn  23568  fbfinnfr  23797  filin  23810  isfil2  23812  infil  23819  fgss2  23830  fgfil  23831  fgcl  23834  fgabs  23835  elfm2  23904  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fmco  23917  flffbas  23951  cnpflf2  23956  fclscf  23981  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  neibl  24457  met2ndc  24479  metcnp3  24496  icccmplem2  24780  xrge0tsms  24791  fgcfil  25239  volfiniun  25516  dyadmax  25567  dyadmbllem  25568  c1liplem1  25969  dgrlem  26202  axcontlem10  29058  usgredg2vtxeuALT  29307  ushgredgedg  29314  ushgredgedgloop  29316  uhgrspan1  29388  nbuhgr2vtx1edgblem  29436  erclwwlksym  30108  erclwwlknsym  30157  1pthon2v  30240  conngrv2edg  30282  lpni  30567  grpoidinvlem3  30593  grporcan  30605  omlsii  31490  spansncol  31655  spansnss  31658  spanunsni  31666  h1datomi  31668  nmopsetretALT  31950  branmfn  32192  chjatom  32444  cvbr4i  32454  atomli  32469  xrge0tsmsd  33166  umgr2cycllem  35353  umgr2cycl  35354  sat1el2xp  35592  fmlasuc  35599  satffunlem1lem2  35616  satffunlem2lem1  35617  satffunlem2lem2  35619  dfon2lem6  35999  colineardim1  36274  finminlem  36531  nn0prpwlem  36535  neibastop2lem  36573  neibastop2  36574  fgmin  36583  exrecfnlem  37631  heiborlem10  38068  prtlem15  39248  lshpcmp  39361  lsatn0  39372  lsatcmp  39376  lsmsat  39381  lsatcv0  39404  l1cvpat  39427  eqlkr  39472  lshpkrlem1  39483  lshpkrlem6  39488  lfl1dim  39494  lfl1dim2N  39495  lkrss2N  39542  athgt  39829  3dim2  39841  llnle  39891  llncmp  39895  lplnle  39913  lplnnle2at  39914  llncvrlpln2  39930  llncvrlpln  39931  lplncmp  39935  lplnexllnN  39937  lvolnle3at  39955  lplncvrlvol2  39988  lplncvrlvol  39989  lvolcmp  39990  pointpsubN  40124  pclfinN  40273  pclfinclN  40323  osumcllem11N  40339  pexmidlem4N  40346  cdleme17d3  40869  cdlemeg46gfre  40905  cdleme48gfv1  40909  cdleme50trn2  40924  trlord  40942  cdlemg6e  40995  cdlemj3  41196  diaelrnN  41418  diaintclN  41431  dia2dimlem6  41442  cdlemm10N  41491  dibintclN  41540  dihord6apre  41629  dihord5b  41632  dihord5apre  41635  dihglblem5apreN  41664  dihglblem2N  41667  dihglblem3N  41668  dihglbcpreN  41673  dihintcl  41717  lclkrlem2y  41904  lcfrvalsnN  41914  isnacs3  43064  jm2.26  43356  fnwe2lem2  43405  hbtlem5  43482  dflim5  43683  uzwo4  45410  iunincfi  45450  restuni3  45474  disjinfi  45548  ssnnf1octb  45550  choicefi  45555  mapssbi  45568  unirnmapsn  45569  iunmapsn  45572  supxrgere  45689  supxrgelem  45693  suplesup  45695  infleinf  45727  suplesup2  45731  rexabslelem  45773  islptre  45976  limcperiod  45985  limclner  46006  limsupmnfuzlem  46081  limsupre3lem  46087  coskpi2  46221  cosknegpi  46224  icccncfext  46242  stoweidlem27  46382  stoweidlem59  46414  fourierdlem41  46503  fourierdlem42  46504  fourierdlem70  46531  fourierdlem71  46532  fourierdlem81  46542  fourierswlem  46585  qndenserrnopnlem  46652  subsaliuncl  46713  subsalsal  46714  sge0tsms  46735  sge0fsum  46742  sge0supre  46744  sge0sup  46746  sge0rnbnd  46748  sge0pnffigt  46751  sge0resrn  46759  sge0split  46764  sge0iunmptlemfi  46768  sge0rpcpnf  46776  sge0isum  46782  sge0xaddlem2  46789  sge0uzfsumgt  46799  sge0seq  46801  sge0reuz  46802  nnfoctbdjlem  46810  nnfoctbdj  46811  meadjiunlem  46820  meaiuninclem  46835  carageniuncllem2  46877  caratheodorylem2  46882  ovnsupge0  46912  ovncvrrp  46919  hoidmv1lelem3  46948  hoidmv1le  46949  hoidmvlelem1  46950  hoidmvlelem2  46951  hoidmvlelem3  46952  ovnhoilem2  46957  opnvonmbllem2  46988  ovnovollem3  47013  sssmf  47093  smfpimbor1lem1  47153  smfco  47157  smfpimcc  47163  smfinflem  47172  fmtno4prmfac  47929  sfprmdvdsmersenne  47960  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  bgoldbtbnd  48166  grimuhgr  48244  clnbgrgrim  48291  uspgrlimlem2  48346