Theorem rexlimdv 3128

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdva  3130  rexlimdva2  3132  rexlimdv3a  3134  rexlimdvw  3135  rexlimdvv  3185  rexlimdvvva  3187  elpwunsn  4638  onelssex  6360  eldmrexrnb  7030  weniso  7295  ssorduni  7719  onint  7730  limuni3  7792  peano5  7833  funcnvuni  7872  funeldmdif  7990  frxp  8066  smoiun  8291  tfrlem9  8314  oaordex  8483  oalimcl  8485  oaass  8486  findcard2  9088  findcard3  9187  findcard3OLD  9188  frfi  9190  unblem1  9197  ordiso2  9426  inf3lem3  9545  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  10481  fpwwe2lem11  10554  tskuni  10696  axgroth6  10741  nqereu  10842  genpnmax  10920  ltaddpr  10947  recexsrlem  11016  mulgt0sr  11018  axrrecex  11076  axpre-sup  11082  addrid  11314  addlid  11317  recex  11770  btwnz  12597  lbzbi  12855  qbtwnre  13119  caubnd  15284  divalglem9  16330  unbenlem  16838  firest  17354  imasmnd2  18666  imasgrp2  18952  pmtrfrn  19355  pgpfi  19502  sylow2blem3  19519  imasrng  20080  imasring  20233  lspsneq  21047  lspdisj  21050  elcls  22976  elcls3  22986  subbascn  23157  cmpsublem  23302  cmpsub  23303  nllyidm  23392  comppfsc  23435  ptpjopn  23515  fbfinnfr  23744  filin  23757  isfil2  23759  infil  23766  fgss2  23777  fgfil  23778  fgcl  23781  fgabs  23782  elfm2  23851  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  fmco  23864  flffbas  23898  cnpflf2  23903  fclscf  23928  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  neibl  24405  met2ndc  24427  metcnp3  24444  icccmplem2  24728  xrge0tsms  24739  fgcfil  25187  volfiniun  25464  dyadmax  25515  dyadmbllem  25516  c1liplem1  25917  dgrlem  26150  axcontlem10  28936  usgredg2vtxeuALT  29185  ushgredgedg  29192  ushgredgedgloop  29194  uhgrspan1  29266  nbuhgr2vtx1edgblem  29314  erclwwlksym  29983  erclwwlknsym  30032  1pthon2v  30115  conngrv2edg  30157  lpni  30442  grpoidinvlem3  30468  grporcan  30480  omlsii  31365  spansncol  31530  spansnss  31533  spanunsni  31541  h1datomi  31543  nmopsetretALT  31825  branmfn  32067  chjatom  32319  cvbr4i  32329  atomli  32344  xrge0tsmsd  33028  umgr2cycllem  35115  umgr2cycl  35116  sat1el2xp  35354  fmlasuc  35361  satffunlem1lem2  35378  satffunlem2lem1  35379  satffunlem2lem2  35381  dfon2lem6  35764  colineardim1  36037  finminlem  36294  nn0prpwlem  36298  neibastop2lem  36336  neibastop2  36337  fgmin  36346  exrecfnlem  37355  heiborlem10  37802  prtlem15  38856  lshpcmp  38969  lsatn0  38980  lsatcmp  38984  lsmsat  38989  lsatcv0  39012  l1cvpat  39035  eqlkr  39080  lshpkrlem1  39091  lshpkrlem6  39096  lfl1dim  39102  lfl1dim2N  39103  lkrss2N  39150  athgt  39438  3dim2  39450  llnle  39500  llncmp  39504  lplnle  39522  lplnnle2at  39523  llncvrlpln2  39539  llncvrlpln  39540  lplncmp  39544  lplnexllnN  39546  lvolnle3at  39564  lplncvrlvol2  39597  lplncvrlvol  39598  lvolcmp  39599  pointpsubN  39733  pclfinN  39882  pclfinclN  39932  osumcllem11N  39948  pexmidlem4N  39955  cdleme17d3  40478  cdlemeg46gfre  40514  cdleme48gfv1  40518  cdleme50trn2  40533  trlord  40551  cdlemg6e  40604  cdlemj3  40805  diaelrnN  41027  diaintclN  41040  dia2dimlem6  41051  cdlemm10N  41100  dibintclN  41149  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dihglblem5apreN  41273  dihglblem2N  41276  dihglblem3N  41277  dihglbcpreN  41282  dihintcl  41326  lclkrlem2y  41513  lcfrvalsnN  41523  isnacs3  42686  jm2.26  42978  fnwe2lem2  43027  hbtlem5  43104  dflim5  43305  uzwo4  45034  iunincfi  45075  restuni3  45099  disjinfi  45173  ssnnf1octb  45175  choicefi  45181  mapssbi  45194  unirnmapsn  45195  iunmapsn  45198  supxrgere  45316  supxrgelem  45320  suplesup  45322  infleinf  45355  suplesup2  45359  rexabslelem  45401  islptre  45604  limcperiod  45613  limclner  45636  limsupmnfuzlem  45711  limsupre3lem  45717  coskpi2  45851  cosknegpi  45854  icccncfext  45872  stoweidlem27  46012  stoweidlem59  46044  fourierdlem41  46133  fourierdlem42  46134  fourierdlem70  46161  fourierdlem71  46162  fourierdlem81  46172  fourierswlem  46215  qndenserrnopnlem  46282  subsaliuncl  46343  subsalsal  46344  sge0tsms  46365  sge0fsum  46372  sge0supre  46374  sge0sup  46376  sge0rnbnd  46378  sge0pnffigt  46381  sge0resrn  46389  sge0split  46394  sge0iunmptlemfi  46398  sge0rpcpnf  46406  sge0isum  46412  sge0xaddlem2  46419  sge0uzfsumgt  46429  sge0seq  46431  sge0reuz  46432  nnfoctbdjlem  46440  nnfoctbdj  46441  meadjiunlem  46450  meaiuninclem  46465  carageniuncllem2  46507  caratheodorylem2  46512  ovnsupge0  46542  ovncvrrp  46549  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  ovnhoilem2  46587  opnvonmbllem2  46618  ovnovollem3  46643  sssmf  46723  smfpimbor1lem1  46783  smfco  46787  smfpimcc  46793  smfinflem  46802  fmtno4prmfac  47560  sfprmdvdsmersenne  47591  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbnd  47797  grimuhgr  47875  clnbgrgrim  47922  uspgrlimlem2  47977