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

Theorem rexlimdvva 3067
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 449 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 3066 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  disjxiun  4681  disjxiunOLD  4682  f1prex  6579  f1o2ndf1  7330  uniinqs  7870  eroveu  7885  eroprf  7888  ralxpmap  7949  unxpdomlem3  8207  finsschain  8314  dffi3  8378  sornom  9137  genpv  9859  genpdm  9862  1re  10077  cnegex  10255  zaddcl  11455  rexanre  14130  o1lo1  14312  lo1resb  14339  o1resb  14341  rlimcn2  14365  climcn2  14367  o1of2  14387  o1rlimmul  14393  lo1add  14401  lo1mul  14402  summo  14492  o1fsum  14589  ntrivcvgmul  14678  prodmolem2  14709  prodmo  14710  dvds2lem  15041  bezoutlem4  15306  dvdsmulgcd  15321  divgcdcoprm0  15426  cncongr1  15428  pcqmul  15605  pcneg  15625  pcadd  15640  4sqlem1  15699  4sqlem2  15700  4sqlem4  15703  mul4sq  15705  4sqlem12  15707  4sqlem13  15708  4sqlem18  15713  vdwmc2  15730  vdwlem7  15738  vdwlem9  15740  vdwlem10  15741  vdwlem11  15742  ramlb  15770  ramub1lem2  15778  imasaddfnlem  16235  imasmnd2  17374  imasgrp2  17577  gaorber  17787  psgnunilem2  17961  psgneu  17972  lsmsubm  18114  lsmsubg  18115  lsmmod  18134  lsmdisj2  18141  pj1eu  18155  efgtlen  18185  efgredlem  18206  efgredeu  18211  efgcpbllemb  18214  frgpuptinv  18230  frgpup3lem  18236  qusabl  18314  frgpnabllem1  18322  frgpnabl  18324  cygabl  18338  dprdsubg  18469  ablfacrp  18511  pgpfac1lem3  18522  imasring  18665  dvdsrtr  18698  lss1d  19011  lsmcl  19131  lsmelval2  19133  lbsextlem2  19207  isnzr2  19311  qsssubdrg  19853  znfld  19957  cygznlem3  19966  psgnghm  19974  lsmcss  20084  mdetunilem7  20472  mdetunilem8  20473  cayleyhamilton0  20742  cayleyhamiltonALT  20744  restbas  21010  ordtbas2  21043  ordtbas  21044  cnhaus  21206  cldllycmp  21346  txbas  21418  ptbasin  21428  txcls  21455  xkoccn  21470  txindis  21485  txlly  21487  txnlly  21488  pthaus  21489  ptrescn  21490  txhaus  21498  tx1stc  21501  txkgen  21503  xkohaus  21504  xkoptsub  21505  xkopt  21506  xkoco1cn  21508  xkoco2cn  21509  xkoinjcn  21538  fmfnfmlem3  21807  fmfnfmlem4  21808  hausflimi  21831  hauspwpwf1  21838  txflf  21857  qustgplem  21971  blin2  22281  prdsxmslem2  22381  xrge0tsms  22684  addcnlem  22714  minveclem3b  23245  pmltpc  23265  evthicc2  23275  dyaddisj  23410  ismbfd  23452  mbfimaopnlem  23467  rolle  23798  dvcnvrelem1  23825  dvcvx  23828  itgsubst  23857  plyf  23999  plypf1  24013  plyadd  24018  plymul  24019  coeeu  24026  dgrlem  24030  coeid  24039  aalioulem6  24137  o1cxp  24746  dchrptlem2  25035  lgsdchr  25125  2sqlem5  25192  2sqlem9  25197  2sqb  25202  pntlemp  25344  pnt3  25346  ostthlem1  25361  ostth3  25372  axcontlem4  25892  axcontlem9  25897  upgrpredgv  26079  edglnl  26083  numedglnl  26084  usgredg4  26154  nbuhgr2vtx1edgb  26293  wwlksnwwlksnonOLD  26880  2pthon3v  26908  umgr3v3e3cycl  27162  3cyclfrgr  27268  n4cyclfrgr  27271  frgrwopreg  27303  2clwwlk2clwwlk  27338  ubthlem3  27856  cdjreui  29419  cdj3i  29428  br8d  29548  xrofsup  29661  xrge0tsmsd  29913  qqhval2  30154  mbfmco2  30455  txpconn  31340  cvmlift2lem10  31420  cvmlift2lem12  31422  cvmlift3lem7  31433  cvmlift3lem8  31434  mclsppslem  31606  br8  31772  br6  31773  br4  31774  noprefixmo  31973  brsegle  32340  tailfb  32497  unbdqndv2  32627  mblfinlem3  33578  ismblfin  33580  itg2addnc  33594  ftc1anc  33623  isbnd2  33712  isbnd3  33713  ssbnd  33717  ispridlc  33999  lshpkrlem6  34720  athgt  35060  3dim1  35071  3dim2  35072  lvolex3N  35142  llncvrlpln2  35161  lplncvrlvol2  35219  linepsubN  35356  lncvrelatN  35385  linepsubclN  35555  eldioph2  37642  eldioph2b  37643  diophin  37653  diophun  37654  fphpdo  37698  irrapxlem3  37705  irrapxlem5  37707  pell1234qrne0  37734  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrgt0  37740  pell14qrdich  37750  pell1qrge1  37751  pell1qrgap  37755  pellqrex  37760  rmxycomplete  37799  jm2.27  37892  stoweidlem49  40584  gbowgt5  41975  m1modmmod  42641
  Copyright terms: Public domain W3C validator