MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdvva Structured version   Visualization version   GIF version

Theorem rexlimdvva 3280
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
Assertion
Ref Expression
rexlimdvva (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21ex 416 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 3279 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2114  wrex 3131
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 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3135  df-rex 3136
This theorem is referenced by:  disjxiun  5039  reuop  6122  f1prex  7023  f1o2ndf1  7805  uniinqs  8364  eroveu  8379  eroprf  8382  ralxpmap  8447  unxpdomlem3  8712  finsschain  8819  dffi3  8883  sornom  9688  genpv  10410  genpdm  10413  1re  10630  cnegex  10810  zaddcl  12010  rexanre  14697  o1lo1  14885  lo1resb  14912  o1resb  14914  rlimcn2  14938  climcn2  14940  o1of2  14960  o1rlimmul  14966  lo1add  14974  lo1mul  14975  summo  15065  o1fsum  15159  ntrivcvgmul  15249  prodmolem2  15280  prodmo  15281  dvds2lem  15613  bezoutlem4  15879  dvdsmulgcd  15894  divgcdcoprm0  15998  cncongr1  16000  pcqmul  16179  pcneg  16199  pcadd  16214  4sqlem1  16273  4sqlem2  16274  4sqlem4  16277  mul4sq  16279  4sqlem12  16281  4sqlem13  16282  4sqlem18  16287  vdwmc2  16304  vdwlem7  16312  vdwlem9  16314  vdwlem10  16315  vdwlem11  16316  ramlb  16344  ramub1lem2  16352  imasaddfnlem  16792  imasmnd2  17939  imasgrp2  18205  cyccom  18337  gaorber  18429  psgnunilem2  18614  psgneu  18625  lsmsubm  18769  lsmsubg  18770  lsmmod  18792  lsmdisj2  18799  pj1eu  18813  efgtlen  18843  efgredlem  18864  efgredeu  18869  efgcpbllemb  18872  frgpuptinv  18888  frgpup3lem  18894  qusabl  18976  frgpnabllem1  18984  frgpnabl  18986  cygablOLD  19002  dprdsubg  19137  ablfacrp  19179  pgpfac1lem3  19190  imasring  19363  dvdsrtr  19396  lss1d  19726  lsmcl  19846  lsmelval2  19848  lbsextlem2  19922  isnzr2  20027  qsssubdrg  20148  znfld  20250  cygznlem3  20259  psgnghm  20267  lsmcss  20379  mdetunilem7  21221  mdetunilem8  21222  cayleyhamilton0  21492  cayleyhamiltonALT  21494  restbas  21761  ordtbas2  21794  ordtbas  21795  cnhaus  21957  cldllycmp  22098  txbas  22170  ptbasin  22180  txcls  22207  xkoccn  22222  txindis  22237  txlly  22239  txnlly  22240  pthaus  22241  ptrescn  22242  txhaus  22250  tx1stc  22253  txkgen  22255  xkohaus  22256  xkoptsub  22257  xkopt  22258  xkoco1cn  22260  xkoco2cn  22261  xkoinjcn  22290  fmfnfmlem3  22559  fmfnfmlem4  22560  hausflimi  22583  hauspwpwf1  22590  txflf  22609  qustgplem  22724  blin2  23034  prdsxmslem2  23134  xrge0tsms  23437  addcnlem  23467  minveclem3b  24030  pmltpc  24052  evthicc2  24062  dyaddisj  24198  ismbfd  24241  mbfimaopnlem  24257  rolle  24591  dvcnvrelem1  24618  dvcvx  24621  itgsubst  24650  plyf  24793  plypf1  24807  plyadd  24812  plymul  24813  coeeu  24820  dgrlem  24824  coeid  24833  aalioulem6  24931  logbgcd1irr  25378  o1cxp  25558  dchrptlem2  25847  lgsdchr  25937  2sqlem5  26004  2sqlem9  26009  2sqb  26014  2sqreulem1  26028  2sqreunnlem1  26031  2sqreunnltblem  26033  pntlemp  26192  pnt3  26194  ostthlem1  26209  ostth3  26220  axcontlem4  26759  axcontlem9  26764  upgrpredgv  26930  edglnl  26934  numedglnl  26935  usgredg4  27005  nbuhgr2vtx1edgb  27140  2pthon3v  27727  umgr3v3e3cycl  27967  3cyclfrgr  28071  n4cyclfrgr  28074  frgrwopreg  28106  2clwwlk2clwwlk  28133  ubthlem3  28653  cdjreui  30213  cdj3i  30222  br8d  30369  xrofsup  30502  xrge0tsmsd  30723  qqhval2  31297  mbfmco2  31597  txpconn  32553  cvmlift2lem10  32633  cvmlift2lem12  32635  cvmlift3lem7  32646  cvmlift3lem8  32647  satfv0  32679  satfv0fun  32692  satffunlem2lem1  32725  mclsppslem  32904  br8  33066  br6  33067  br4  33068  frrlem9  33205  noprefixmo  33276  brsegle  33643  tailfb  33799  unbdqndv2  33924  mblfinlem3  35054  ismblfin  35056  itg2addnc  35069  ftc1anc  35096  isbnd2  35179  isbnd3  35180  ssbnd  35184  ispridlc  35466  lshpkrlem6  36369  athgt  36710  3dim1  36721  3dim2  36722  lvolex3N  36792  llncvrlpln2  36811  lplncvrlvol2  36869  linepsubN  37006  lncvrelatN  37035  linepsubclN  37205  fsuppind  39403  sn-negex12  39497  eldioph2  39633  eldioph2b  39634  diophin  39643  diophun  39644  fphpdo  39688  irrapxlem3  39695  irrapxlem5  39697  pell1234qrne0  39724  pell1234qrreccl  39725  pell1234qrmulcl  39726  pell14qrgt0  39730  pell14qrdich  39740  pell1qrge1  39741  pell1qrgap  39745  pellqrex  39750  rmxycomplete  39788  jm2.27  39879  stoweidlem49  42630  ichreuopeq  43929  prproropf1olem2  43960  prproropf1olem4  43962  paireqne  43967  reupr  43978  requad2  44080  gbowgt5  44219  isomuspgrlem1  44284  isomuspgrlem2b  44286  isomuspgrlem2d  44288  m1modmmod  44874  prelrrx2b  45067
  Copyright terms: Public domain W3C validator