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

Theorem rexlimdvva 3019
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 448 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
32rexlimdvv 3018 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  disjxiun  4573  disjxiunOLD  4574  f1prex  6417  f1o2ndf1  7149  uniinqs  7691  eroveu  7706  eroprf  7709  ralxpmap  7770  unxpdomlem3  8028  finsschain  8133  dffi3  8197  sornom  8959  genpv  9677  genpdm  9680  1re  9895  cnegex  10068  zaddcl  11250  rexanre  13880  o1lo1  14062  lo1resb  14089  o1resb  14091  rlimcn2  14115  climcn2  14117  o1of2  14137  o1rlimmul  14143  lo1add  14151  lo1mul  14152  summo  14241  o1fsum  14332  ntrivcvgmul  14419  prodmolem2  14450  prodmo  14451  dvds2lem  14778  bezoutlem4  15043  dvdsmulgcd  15058  divgcdcoprm0  15163  cncongr1  15165  pcqmul  15342  pcneg  15362  pcadd  15377  4sqlem1  15436  4sqlem2  15437  4sqlem4  15440  mul4sq  15442  4sqlem12  15444  4sqlem13  15445  4sqlem18  15450  vdwmc2  15467  vdwlem7  15475  vdwlem9  15477  vdwlem10  15478  vdwlem11  15479  ramlb  15507  ramub1lem2  15515  imasaddfnlem  15957  imasmnd2  17096  imasgrp2  17299  gaorber  17510  psgnunilem2  17684  psgneu  17695  lsmsubm  17837  lsmsubg  17838  lsmmod  17857  lsmdisj2  17864  pj1eu  17878  efgtlen  17908  efgredlem  17929  efgredeu  17934  efgcpbllemb  17937  frgpuptinv  17953  frgpup3lem  17959  qusabl  18037  frgpnabllem1  18045  frgpnabl  18047  cygabl  18061  dprdsubg  18192  ablfacrp  18234  pgpfac1lem3  18245  imasring  18388  dvdsrtr  18421  lss1d  18730  lsmcl  18850  lsmelval2  18852  lbsextlem2  18926  isnzr2  19030  qsssubdrg  19570  znfld  19673  cygznlem3  19682  psgnghm  19690  lsmcss  19797  mdetunilem7  20185  mdetunilem8  20186  cayleyhamilton0  20455  cayleyhamiltonALT  20457  restbas  20714  ordtbas2  20747  ordtbas  20748  cnhaus  20910  cldllycmp  21050  txbas  21122  ptbasin  21132  txcls  21159  xkoccn  21174  txindis  21189  txlly  21191  txnlly  21192  pthaus  21193  ptrescn  21194  txhaus  21202  tx1stc  21205  txkgen  21207  xkohaus  21208  xkoptsub  21209  xkopt  21210  xkoco1cn  21212  xkoco2cn  21213  xkoinjcn  21242  fmfnfmlem3  21512  fmfnfmlem4  21513  hausflimi  21536  hauspwpwf1  21543  txflf  21562  qustgplem  21676  blin2  21985  prdsxmslem2  22085  xrge0tsms  22377  addcnlem  22406  minveclem3b  22924  pmltpc  22943  evthicc2  22953  dyaddisj  23087  ismbfd  23130  mbfimaopnlem  23145  rolle  23474  dvcnvrelem1  23501  dvcvx  23504  itgsubst  23533  plyf  23675  plypf1  23689  plyadd  23694  plymul  23695  coeeu  23702  dgrlem  23706  coeid  23715  aalioulem6  23813  o1cxp  24418  dchrptlem2  24707  lgsdchr  24797  2sqlem5  24864  2sqlem9  24869  2sqb  24874  pntlemp  25016  pnt3  25018  ostthlem1  25033  ostth3  25044  axcontlem4  25565  axcontlem9  25570  sizeusglecusglem1  25778  el2wlksotot  26175  3cyclfrgra  26308  n4cyclfrgra  26311  frgrawopreg  26342  ubthlem3  26918  cdjreui  28481  cdj3i  28490  br8d  28608  xrofsup  28729  xrge0tsmsd  28922  qqhval2  29160  mbfmco2  29460  txpcon  30274  cvmlift2lem10  30354  cvmlift2lem12  30356  cvmlift3lem7  30367  cvmlift3lem8  30368  mclsppslem  30540  br8  30705  br6  30706  br4  30707  brsegle  31191  tailfb  31348  unbdqndv2  31478  mblfinlem3  32414  ismblfin  32416  itg2addnc  32430  ftc1anc  32459  isbnd2  32548  isbnd3  32549  ssbnd  32553  ispridlc  32835  lshpkrlem6  33216  athgt  33556  3dim1  33567  3dim2  33568  lvolex3N  33638  llncvrlpln2  33657  lplncvrlvol2  33715  linepsubN  33852  lncvrelatN  33881  linepsubclN  34051  eldioph2  36139  eldioph2b  36140  diophin  36150  diophun  36151  fphpdo  36195  irrapxlem3  36202  irrapxlem5  36204  pell1234qrne0  36231  pell1234qrreccl  36232  pell1234qrmulcl  36233  pell14qrgt0  36237  pell14qrdich  36247  pell1qrge1  36248  pell1qrgap  36252  pellqrex  36257  rmxycomplete  36296  jm2.27  36389  stoweidlem49  38739  gbogt5  39982  usgredg4  40439  nbuhgr2vtx1edgb  40569  wwlksnwwlksnon  41116  2pthon3v-av  41145  umgr3v3e3cycl  41346  3cyclfrgr  41453  n4cyclfrgr  41456  frgrwopreg  41481  m1modmmod  42105
  Copyright terms: Public domain W3C validator