Theorem rexlimdv 3148

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-rex 3066

This theorem is referenced by:  rexlimdva  3150  rexlimdva2  3152  rexlimdv3a  3154  rexlimdvw  3155  rexlimdvv  3205  elpwunsn  4683  onelssex  6411  eldmrexrnb  7096  weniso  7356  ssorduni  7775  onint  7787  limuni3  7850  peano5  7893  funcnvuni  7933  funeldmdif  8046  frxp  8125  smoiun  8375  tfrlem9  8399  oaordex  8572  oalimcl  8574  oaass  8575  findcard2  9180  findcard3  9301  findcard3OLD  9302  frfi  9304  unblem1  9311  ordiso2  9530  inf3lem3  9645  r1sdom  9789  tz9.12lem3  9804  karden  9910  infxpenlem  10028  cardinfima  10112  iunfictbso  10129  dfac5  10143  cfcoflem  10287  fin23lem11  10332  fin23lem30  10357  fin1a2lem13  10427  axdc3lem2  10466  konigthlem  10583  fpwwe2lem11  10656  tskuni  10798  axgroth6  10843  nqereu  10944  genpnmax  11022  ltaddpr  11049  recexsrlem  11118  mulgt0sr  11120  axrrecex  11178  axpre-sup  11184  addrid  11416  addlid  11419  recex  11868  btwnz  12687  lbzbi  12942  qbtwnre  13202  caubnd  15329  divalglem9  16369  unbenlem  16868  firest  17405  imasmnd2  18722  imasgrp2  19002  pmtrfrn  19404  pgpfi  19551  sylow2blem3  19568  imasrng  20108  imasring  20255  lspsneq  20999  lspdisj  21002  elcls  22964  elcls3  22974  subbascn  23145  cmpsublem  23290  cmpsub  23291  nllyidm  23380  comppfsc  23423  ptpjopn  23503  fbfinnfr  23732  filin  23745  isfil2  23747  infil  23754  fgss2  23765  fgfil  23766  fgcl  23769  fgabs  23770  elfm2  23839  rnelfm  23844  fmfnfmlem2  23846  fmfnfmlem4  23848  fmco  23852  flffbas  23886  cnpflf2  23891  fclscf  23916  alexsubALTlem2  23939  alexsubALTlem3  23940  alexsubALTlem4  23941  alexsubALT  23942  neibl  24397  met2ndc  24419  metcnp3  24436  icccmplem2  24726  xrge0tsms  24737  fgcfil  25186  volfiniun  25463  dyadmax  25514  dyadmbllem  25515  c1liplem1  25916  dgrlem  26150  axcontlem10  28771  usgredg2vtxeuALT  29022  ushgredgedg  29029  ushgredgedgloop  29031  uhgrspan1  29103  nbuhgr2vtx1edgblem  29151  erclwwlksym  29818  erclwwlknsym  29867  1pthon2v  29950  conngrv2edg  29992  lpni  30277  grpoidinvlem3  30303  grporcan  30315  omlsii  31200  spansncol  31365  spansnss  31368  spanunsni  31376  h1datomi  31378  nmopsetretALT  31660  branmfn  31902  chjatom  32154  cvbr4i  32164  atomli  32179  xrge0tsmsd  32749  umgr2cycllem  34686  umgr2cycl  34687  sat1el2xp  34925  fmlasuc  34932  satffunlem1lem2  34949  satffunlem2lem1  34950  satffunlem2lem2  34952  dfon2lem6  35320  colineardim1  35593  finminlem  35738  nn0prpwlem  35742  neibastop2lem  35780  neibastop2  35781  fgmin  35790  exrecfnlem  36794  heiborlem10  37228  prtlem15  38284  lshpcmp  38397  lsatn0  38408  lsatcmp  38412  lsmsat  38417  lsatcv0  38440  l1cvpat  38463  eqlkr  38508  lshpkrlem1  38519  lshpkrlem6  38524  lfl1dim  38530  lfl1dim2N  38531  lkrss2N  38578  athgt  38866  3dim2  38878  llnle  38928  llncmp  38932  lplnle  38950  lplnnle2at  38951  llncvrlpln2  38967  llncvrlpln  38968  lplncmp  38972  lplnexllnN  38974  lvolnle3at  38992  lplncvrlvol2  39025  lplncvrlvol  39026  lvolcmp  39027  pointpsubN  39161  pclfinN  39310  pclfinclN  39360  osumcllem11N  39376  pexmidlem4N  39383  cdleme17d3  39906  cdlemeg46gfre  39942  cdleme48gfv1  39946  cdleme50trn2  39961  trlord  39979  cdlemg6e  40032  cdlemj3  40233  diaelrnN  40455  diaintclN  40468  dia2dimlem6  40479  cdlemm10N  40528  dibintclN  40577  dihord6apre  40666  dihord5b  40669  dihord5apre  40672  dihglblem5apreN  40701  dihglblem2N  40704  dihglblem3N  40705  dihglbcpreN  40710  dihintcl  40754  lclkrlem2y  40941  lcfrvalsnN  40951  isnacs3  42052  jm2.26  42345  fnwe2lem2  42397  hbtlem5  42474  dflim5  42681  uzwo4  44340  iunincfi  44383  restuni3  44407  disjinfi  44488  ssnnf1octb  44490  choicefi  44496  mapssbi  44509  unirnmapsn  44510  ssmapsn  44512  iunmapsn  44513  supxrgere  44638  supxrgelem  44642  suplesup  44644  infleinf  44677  suplesup2  44681  rexabslelem  44723  islptre  44930  limcperiod  44939  limclner  44962  limsupmnfuzlem  45037  limsupre3lem  45043  coskpi2  45177  cosknegpi  45180  icccncfext  45198  stoweidlem27  45338  stoweidlem59  45370  fourierdlem41  45459  fourierdlem42  45460  fourierdlem70  45487  fourierdlem71  45488  fourierdlem81  45498  fourierswlem  45541  qndenserrnopnlem  45608  subsaliuncl  45669  subsalsal  45670  sge0tsms  45691  sge0fsum  45698  sge0supre  45700  sge0sup  45702  sge0rnbnd  45704  sge0pnffigt  45707  sge0resrn  45715  sge0split  45720  sge0iunmptlemfi  45724  sge0rpcpnf  45732  sge0isum  45738  sge0xaddlem2  45745  sge0uzfsumgt  45755  sge0seq  45757  sge0reuz  45758  nnfoctbdjlem  45766  nnfoctbdj  45767  meadjiunlem  45776  meaiuninclem  45791  carageniuncllem2  45833  caratheodorylem2  45838  ovnsupge0  45868  ovncvrrp  45875  hoidmv1lelem3  45904  hoidmv1le  45905  hoidmvlelem1  45906  hoidmvlelem2  45907  hoidmvlelem3  45908  ovnhoilem2  45913  opnvonmbllem2  45944  ovnovollem3  45969  sssmf  46049  smfpimbor1lem1  46109  smfco  46113  smfpimcc  46119  smfinflem  46128  fmtno4prmfac  46835  sfprmdvdsmersenne  46866  nnsum4primeseven  47063  nnsum4primesevenALTV  47064  bgoldbtbnd  47072  grimuhgr  47099