Theorem rexlimdv 3132

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 3127	. 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  3134  rexlimdva2  3136  rexlimdv3a  3138  rexlimdvw  3139  rexlimdvv  3193  rexlimdvvva  3195  elpwunsn  4648  onelssex  6381  eldmrexrnb  7064  weniso  7329  ssorduni  7755  onint  7766  limuni3  7828  peano5  7869  funcnvuni  7908  funeldmdif  8027  frxp  8105  smoiun  8330  tfrlem9  8353  oaordex  8522  oalimcl  8524  oaass  8525  findcard2  9128  findcard3  9229  findcard3OLD  9230  frfi  9232  unblem1  9239  ordiso2  9468  inf3lem3  9583  r1sdom  9727  tz9.12lem3  9742  karden  9848  infxpenlem  9966  cardinfima  10050  iunfictbso  10067  dfac5  10082  cfcoflem  10225  fin23lem11  10270  fin23lem30  10295  fin1a2lem13  10365  axdc3lem2  10404  konigthlem  10521  fpwwe2lem11  10594  tskuni  10736  axgroth6  10781  nqereu  10882  genpnmax  10960  ltaddpr  10987  recexsrlem  11056  mulgt0sr  11058  axrrecex  11116  axpre-sup  11122  addrid  11354  addlid  11357  recex  11810  btwnz  12637  lbzbi  12895  qbtwnre  13159  caubnd  15325  divalglem9  16371  unbenlem  16879  firest  17395  imasmnd2  18701  imasgrp2  18987  pmtrfrn  19388  pgpfi  19535  sylow2blem3  19552  imasrng  20086  imasring  20239  lspsneq  21032  lspdisj  21035  elcls  22960  elcls3  22970  subbascn  23141  cmpsublem  23286  cmpsub  23287  nllyidm  23376  comppfsc  23419  ptpjopn  23499  fbfinnfr  23728  filin  23741  isfil2  23743  infil  23750  fgss2  23761  fgfil  23762  fgcl  23765  fgabs  23766  elfm2  23835  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fmco  23848  flffbas  23882  cnpflf2  23887  fclscf  23912  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  neibl  24389  met2ndc  24411  metcnp3  24428  icccmplem2  24712  xrge0tsms  24723  fgcfil  25171  volfiniun  25448  dyadmax  25499  dyadmbllem  25500  c1liplem1  25901  dgrlem  26134  axcontlem10  28900  usgredg2vtxeuALT  29149  ushgredgedg  29156  ushgredgedgloop  29158  uhgrspan1  29230  nbuhgr2vtx1edgblem  29278  erclwwlksym  29950  erclwwlknsym  29999  1pthon2v  30082  conngrv2edg  30124  lpni  30409  grpoidinvlem3  30435  grporcan  30447  omlsii  31332  spansncol  31497  spansnss  31500  spanunsni  31508  h1datomi  31510  nmopsetretALT  31792  branmfn  32034  chjatom  32286  cvbr4i  32296  atomli  32311  xrge0tsmsd  33002  umgr2cycllem  35127  umgr2cycl  35128  sat1el2xp  35366  fmlasuc  35373  satffunlem1lem2  35390  satffunlem2lem1  35391  satffunlem2lem2  35393  dfon2lem6  35776  colineardim1  36049  finminlem  36306  nn0prpwlem  36310  neibastop2lem  36348  neibastop2  36349  fgmin  36358  exrecfnlem  37367  heiborlem10  37814  prtlem15  38868  lshpcmp  38981  lsatn0  38992  lsatcmp  38996  lsmsat  39001  lsatcv0  39024  l1cvpat  39047  eqlkr  39092  lshpkrlem1  39103  lshpkrlem6  39108  lfl1dim  39114  lfl1dim2N  39115  lkrss2N  39162  athgt  39450  3dim2  39462  llnle  39512  llncmp  39516  lplnle  39534  lplnnle2at  39535  llncvrlpln2  39551  llncvrlpln  39552  lplncmp  39556  lplnexllnN  39558  lvolnle3at  39576  lplncvrlvol2  39609  lplncvrlvol  39610  lvolcmp  39611  pointpsubN  39745  pclfinN  39894  pclfinclN  39944  osumcllem11N  39960  pexmidlem4N  39967  cdleme17d3  40490  cdlemeg46gfre  40526  cdleme48gfv1  40530  cdleme50trn2  40545  trlord  40563  cdlemg6e  40616  cdlemj3  40817  diaelrnN  41039  diaintclN  41052  dia2dimlem6  41063  cdlemm10N  41112  dibintclN  41161  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihglblem5apreN  41285  dihglblem2N  41288  dihglblem3N  41289  dihglbcpreN  41294  dihintcl  41338  lclkrlem2y  41525  lcfrvalsnN  41535  isnacs3  42698  jm2.26  42991  fnwe2lem2  43040  hbtlem5  43117  dflim5  43318  uzwo4  45047  iunincfi  45088  restuni3  45112  disjinfi  45186  ssnnf1octb  45188  choicefi  45194  mapssbi  45207  unirnmapsn  45208  iunmapsn  45211  supxrgere  45329  supxrgelem  45333  suplesup  45335  infleinf  45368  suplesup2  45372  rexabslelem  45414  islptre  45617  limcperiod  45626  limclner  45649  limsupmnfuzlem  45724  limsupre3lem  45730  coskpi2  45864  cosknegpi  45867  icccncfext  45885  stoweidlem27  46025  stoweidlem59  46057  fourierdlem41  46146  fourierdlem42  46147  fourierdlem70  46174  fourierdlem71  46175  fourierdlem81  46185  fourierswlem  46228  qndenserrnopnlem  46295  subsaliuncl  46356  subsalsal  46357  sge0tsms  46378  sge0fsum  46385  sge0supre  46387  sge0sup  46389  sge0rnbnd  46391  sge0pnffigt  46394  sge0resrn  46402  sge0split  46407  sge0iunmptlemfi  46411  sge0rpcpnf  46419  sge0isum  46425  sge0xaddlem2  46432  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  nnfoctbdjlem  46453  nnfoctbdj  46454  meadjiunlem  46463  meaiuninclem  46478  carageniuncllem2  46520  caratheodorylem2  46525  ovnsupge0  46555  ovncvrrp  46562  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem2  46600  opnvonmbllem2  46631  ovnovollem3  46656  sssmf  46736  smfpimbor1lem1  46796  smfco  46800  smfpimcc  46806  smfinflem  46815  fmtno4prmfac  47573  sfprmdvdsmersenne  47604  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbnd  47810  grimuhgr  47887  clnbgrgrim  47934  uspgrlimlem2  47988