Theorem rexlimdv 3159

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimdva  3161  rexlimdva2  3163  rexlimdv3a  3165  rexlimdvw  3166  rexlimdvv  3218  rexlimdvvva  3220  elpwunsn  4707  onelssex  6443  eldmrexrnb  7126  weniso  7390  ssorduni  7814  onint  7826  limuni3  7889  peano5  7932  funcnvuni  7972  funeldmdif  8089  frxp  8167  smoiun  8417  tfrlem9  8441  oaordex  8614  oalimcl  8616  oaass  8617  findcard2  9230  findcard3  9346  findcard3OLD  9347  frfi  9349  unblem1  9356  ordiso2  9584  inf3lem3  9699  r1sdom  9843  tz9.12lem3  9858  karden  9964  infxpenlem  10082  cardinfima  10166  iunfictbso  10183  dfac5  10198  cfcoflem  10341  fin23lem11  10386  fin23lem30  10411  fin1a2lem13  10481  axdc3lem2  10520  konigthlem  10637  fpwwe2lem11  10710  tskuni  10852  axgroth6  10897  nqereu  10998  genpnmax  11076  ltaddpr  11103  recexsrlem  11172  mulgt0sr  11174  axrrecex  11232  axpre-sup  11238  addrid  11470  addlid  11473  recex  11922  btwnz  12746  lbzbi  13001  qbtwnre  13261  caubnd  15407  divalglem9  16449  unbenlem  16955  firest  17492  imasmnd2  18809  imasgrp2  19095  pmtrfrn  19500  pgpfi  19647  sylow2blem3  19664  imasrng  20204  imasring  20353  lspsneq  21147  lspdisj  21150  elcls  23102  elcls3  23112  subbascn  23283  cmpsublem  23428  cmpsub  23429  nllyidm  23518  comppfsc  23561  ptpjopn  23641  fbfinnfr  23870  filin  23883  isfil2  23885  infil  23892  fgss2  23903  fgfil  23904  fgcl  23907  fgabs  23908  elfm2  23977  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  fmco  23990  flffbas  24024  cnpflf2  24029  fclscf  24054  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  neibl  24535  met2ndc  24557  metcnp3  24574  icccmplem2  24864  xrge0tsms  24875  fgcfil  25324  volfiniun  25601  dyadmax  25652  dyadmbllem  25653  c1liplem1  26055  dgrlem  26288  axcontlem10  29006  usgredg2vtxeuALT  29257  ushgredgedg  29264  ushgredgedgloop  29266  uhgrspan1  29338  nbuhgr2vtx1edgblem  29386  erclwwlksym  30053  erclwwlknsym  30102  1pthon2v  30185  conngrv2edg  30227  lpni  30512  grpoidinvlem3  30538  grporcan  30550  omlsii  31435  spansncol  31600  spansnss  31603  spanunsni  31611  h1datomi  31613  nmopsetretALT  31895  branmfn  32137  chjatom  32389  cvbr4i  32399  atomli  32414  xrge0tsmsd  33041  umgr2cycllem  35108  umgr2cycl  35109  sat1el2xp  35347  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  dfon2lem6  35752  colineardim1  36025  finminlem  36284  nn0prpwlem  36288  neibastop2lem  36326  neibastop2  36327  fgmin  36336  exrecfnlem  37345  heiborlem10  37780  prtlem15  38831  lshpcmp  38944  lsatn0  38955  lsatcmp  38959  lsmsat  38964  lsatcv0  38987  l1cvpat  39010  eqlkr  39055  lshpkrlem1  39066  lshpkrlem6  39071  lfl1dim  39077  lfl1dim2N  39078  lkrss2N  39125  athgt  39413  3dim2  39425  llnle  39475  llncmp  39479  lplnle  39497  lplnnle2at  39498  llncvrlpln2  39514  llncvrlpln  39515  lplncmp  39519  lplnexllnN  39521  lvolnle3at  39539  lplncvrlvol2  39572  lplncvrlvol  39573  lvolcmp  39574  pointpsubN  39708  pclfinN  39857  pclfinclN  39907  osumcllem11N  39923  pexmidlem4N  39930  cdleme17d3  40453  cdlemeg46gfre  40489  cdleme48gfv1  40493  cdleme50trn2  40508  trlord  40526  cdlemg6e  40579  cdlemj3  40780  diaelrnN  41002  diaintclN  41015  dia2dimlem6  41026  cdlemm10N  41075  dibintclN  41124  dihord6apre  41213  dihord5b  41216  dihord5apre  41219  dihglblem5apreN  41248  dihglblem2N  41251  dihglblem3N  41252  dihglbcpreN  41257  dihintcl  41301  lclkrlem2y  41488  lcfrvalsnN  41498  isnacs3  42666  jm2.26  42959  fnwe2lem2  43008  hbtlem5  43085  dflim5  43291  uzwo4  44955  iunincfi  44996  restuni3  45020  disjinfi  45099  ssnnf1octb  45101  choicefi  45107  mapssbi  45120  unirnmapsn  45121  ssmapsn  45123  iunmapsn  45124  supxrgere  45248  supxrgelem  45252  suplesup  45254  infleinf  45287  suplesup2  45291  rexabslelem  45333  islptre  45540  limcperiod  45549  limclner  45572  limsupmnfuzlem  45647  limsupre3lem  45653  coskpi2  45787  cosknegpi  45790  icccncfext  45808  stoweidlem27  45948  stoweidlem59  45980  fourierdlem41  46069  fourierdlem42  46070  fourierdlem70  46097  fourierdlem71  46098  fourierdlem81  46108  fourierswlem  46151  qndenserrnopnlem  46218  subsaliuncl  46279  subsalsal  46280  sge0tsms  46301  sge0fsum  46308  sge0supre  46310  sge0sup  46312  sge0rnbnd  46314  sge0pnffigt  46317  sge0resrn  46325  sge0split  46330  sge0iunmptlemfi  46334  sge0rpcpnf  46342  sge0isum  46348  sge0xaddlem2  46355  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  nnfoctbdjlem  46376  nnfoctbdj  46377  meadjiunlem  46386  meaiuninclem  46401  carageniuncllem2  46443  caratheodorylem2  46448  ovnsupge0  46478  ovncvrrp  46485  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem2  46523  opnvonmbllem2  46554  ovnovollem3  46579  sssmf  46659  smfpimbor1lem1  46719  smfco  46723  smfpimcc  46729  smfinflem  46738  fmtno4prmfac  47446  sfprmdvdsmersenne  47477  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbnd  47683  grimuhgr  47762  clnbgrgrim  47786  uspgrlimlem2  47813