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

Theorem rexlimdvva 3206
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 414 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 3205 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  disjxiun  5103  reuop  6246  f1prex  7231  f1o2ndf1  8055  poxp2  8076  xpord2pred  8078  sexp2  8079  xpord3pred  8085  sexp3  8086  frrlem9  8226  uniinqs  8737  eroveu  8752  eroprf  8755  ralxpmap  8835  unxpdomlem3  9197  finsschain  9304  dffi3  9368  sornom  10214  genpv  10936  genpdm  10939  1re  11156  cnegex  11337  zaddcl  12544  rexanre  15232  o1lo1  15420  lo1resb  15447  o1resb  15449  rlimcn3  15473  climcn2  15476  o1of2  15496  o1rlimmul  15502  lo1add  15510  lo1mul  15511  summo  15603  o1fsum  15699  ntrivcvgmul  15788  prodmolem2  15819  prodmo  15820  dvds2lem  16152  bezoutlem4  16424  dvdsmulgcd  16437  divgcdcoprm0  16542  cncongr1  16544  pcqmul  16726  pcneg  16747  pcadd  16762  4sqlem1  16821  4sqlem2  16822  4sqlem4  16825  mul4sq  16827  4sqlem12  16829  4sqlem13  16830  4sqlem18  16835  vdwmc2  16852  vdwlem7  16860  vdwlem9  16862  vdwlem10  16863  vdwlem11  16864  ramlb  16892  ramub1lem2  16900  imasaddfnlem  17411  imasmnd2  18594  imasgrp2  18863  cyccom  18997  gaorber  19089  psgnunilem2  19278  psgneu  19289  lsmsubm  19436  lsmsubg  19437  lsmmod  19458  lsmdisj2  19465  pj1eu  19479  efgtlen  19509  efgredlem  19530  efgredeu  19535  efgcpbllemb  19538  frgpuptinv  19554  frgpup3lem  19560  qusabl  19644  frgpnabllem1  19652  frgpnabl  19654  dprdsubg  19804  ablfacrp  19846  pgpfac1lem3  19857  imasring  20046  dvdsrtr  20082  lss1d  20427  lsmcl  20547  lsmelval2  20549  lbsextlem2  20623  isnzr2  20736  qsssubdrg  20859  znfld  20970  cygznlem3  20979  psgnghm  20987  lsmcss  21099  mdetunilem7  21970  mdetunilem8  21971  cayleyhamilton0  22241  cayleyhamiltonALT  22243  restbas  22512  ordtbas2  22545  ordtbas  22546  cnhaus  22708  cldllycmp  22849  txbas  22921  ptbasin  22931  txcls  22958  xkoccn  22973  txindis  22988  txlly  22990  txnlly  22991  pthaus  22992  ptrescn  22993  txhaus  23001  tx1stc  23004  txkgen  23006  xkohaus  23007  xkoptsub  23008  xkopt  23009  xkoco1cn  23011  xkoco2cn  23012  xkoinjcn  23041  fmfnfmlem3  23310  fmfnfmlem4  23311  hausflimi  23334  hauspwpwf1  23341  txflf  23360  qustgplem  23475  blin2  23785  prdsxmslem2  23888  xrge0tsms  24200  addcnlem  24230  minveclem3b  24795  pmltpc  24817  evthicc2  24827  dyaddisj  24963  ismbfd  25006  mbfimaopnlem  25022  rolle  25357  dvcnvrelem1  25384  dvcvx  25387  itgsubst  25416  plyf  25562  plypf1  25576  plyadd  25581  plymul  25582  coeeu  25589  dgrlem  25593  coeid  25602  aalioulem6  25700  logbgcd1irr  26147  o1cxp  26327  dchrptlem2  26616  lgsdchr  26706  2sqlem5  26773  2sqlem9  26778  2sqb  26783  2sqreulem1  26797  2sqreunnlem1  26800  2sqreunnltblem  26802  pntlemp  26961  pnt3  26963  ostthlem1  26978  ostth3  26989  nosupprefixmo  27051  noinfprefixmo  27052  addsproplem2  27285  negsproplem2  27330  axcontlem4  27919  axcontlem9  27924  upgrpredgv  28093  edglnl  28097  numedglnl  28098  usgredg4  28168  nbuhgr2vtx1edgb  28303  2pthon3v  28891  umgr3v3e3cycl  29131  3cyclfrgr  29235  n4cyclfrgr  29238  frgrwopreg  29270  2clwwlk2clwwlk  29297  ubthlem3  29817  cdjreui  31377  cdj3i  31386  br8d  31532  xrofsup  31675  xrge0tsmsd  31902  qqhval2  32566  mbfmco2  32868  txpconn  33829  cvmlift2lem10  33909  cvmlift2lem12  33911  cvmlift3lem7  33922  cvmlift3lem8  33923  satfv0  33955  satfv0fun  33968  satffunlem2lem1  34001  mclsppslem  34180  br8  34332  br6  34333  br4  34334  brsegle  34696  tailfb  34852  unbdqndv2  34977  mblfinlem3  36120  ismblfin  36122  itg2addnc  36135  ftc1anc  36162  isbnd2  36245  isbnd3  36246  ssbnd  36250  ispridlc  36532  lshpkrlem6  37580  athgt  37922  3dim1  37933  3dim2  37934  lvolex3N  38004  llncvrlpln2  38023  lplncvrlvol2  38081  linepsubN  38218  lncvrelatN  38247  linepsubclN  38417  fsuppind  40768  sn-negex12  40888  flt4lem7  41000  nna4b4nsq  41001  eldioph2  41088  eldioph2b  41089  diophin  41098  diophun  41099  fphpdo  41143  irrapxlem3  41150  irrapxlem5  41152  pell1234qrne0  41179  pell1234qrreccl  41180  pell1234qrmulcl  41181  pell14qrgt0  41185  pell14qrdich  41195  pell1qrge1  41196  pell1qrgap  41200  pellqrex  41205  rmxycomplete  41244  jm2.27  41335  stoweidlem49  44297  ichreuopeq  45672  prproropf1olem2  45703  prproropf1olem4  45705  paireqne  45710  reupr  45721  requad2  45822  gbowgt5  45961  isomuspgrlem1  46026  isomuspgrlem2b  46028  isomuspgrlem2d  46030  m1modmmod  46614  prelrrx2b  46807
  Copyright terms: Public domain W3C validator