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

Theorem rexlimdvva 2829
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdvva  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, y, ph    ch, x, y    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  ->  ch ) )
21ex 424 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2828 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  disjxiun  4201  f1o2ndf1  6445  uniinqs  6975  eroveu  6990  eroprf  6993  unxpdomlem3  7306  finsschain  7404  dffi3  7427  sornom  8146  genpv  8865  genpdm  8868  1re  9079  cnegex  9236  zaddcl  10306  rexanre  12138  o1lo1  12319  lo1resb  12346  o1resb  12348  rlimcn2  12372  climcn2  12374  o1of2  12394  o1rlimmul  12400  lo1add  12408  lo1mul  12409  summo  12499  o1fsum  12580  dvds2lem  12850  bezoutlem4  13029  dvdsmulgcd  13042  pcqmul  13215  pcneg  13235  pcadd  13246  4sqlem1  13304  4sqlem2  13305  4sqlem4  13308  mul4sq  13310  4sqlem12  13312  4sqlem13  13313  4sqlem18  13318  vdwmc2  13335  vdwlem7  13343  vdwlem9  13345  vdwlem10  13346  vdwlem11  13347  ramlb  13375  ramub1lem2  13383  imasaddfnlem  13741  imasmnd2  14720  imasgrp2  14921  gaorber  15073  lsmsubm  15275  lsmsubg  15276  lsmmod  15295  lsmdisj2  15302  pj1eu  15316  efgtlen  15346  efgredlem  15367  efgredeu  15372  efgcpbllemb  15375  frgpuptinv  15391  frgpup3lem  15397  divsabl  15468  frgpnabllem1  15472  frgpnabl  15474  cygabl  15488  dprdsubg  15570  ablfacrp  15612  pgpfac1lem3  15623  imasrng  15713  dvdsrtr  15745  lss1d  16027  lsmcl  16143  lsmelval2  16145  lbsextlem2  16219  isnzr2  16322  qsssubdrg  16746  znfld  16829  cygznlem3  16838  lsmcss  16907  restbas  17210  ordtbas2  17243  ordtbas  17244  cnhaus  17406  cldllycmp  17546  txbas  17587  ptbasin  17597  txcls  17624  xkoccn  17639  txindis  17654  txlly  17656  txnlly  17657  pthaus  17658  ptrescn  17659  txhaus  17667  tx1stc  17670  txkgen  17672  xkohaus  17673  xkoptsub  17674  xkopt  17675  xkoco1cn  17677  xkoco2cn  17678  xkoinjcn  17707  fmfnfmlem3  17976  fmfnfmlem4  17977  hausflimi  18000  hauspwpwf1  18007  txflf  18026  divstgplem  18138  blin2  18447  prdsxmslem2  18547  xrge0tsms  18853  addcnlem  18882  minveclem3b  19317  pmltpc  19335  evthicc2  19345  dyaddisj  19476  ismbfd  19520  mbfimaopnlem  19535  rolle  19862  dvcnvrelem1  19889  dvcvx  19892  itgsubst  19921  plyf  20105  plypf1  20119  plyadd  20124  plymul  20125  coeeu  20132  dgrlem  20136  coeid  20145  aalioulem6  20242  o1cxp  20801  dchrptlem2  21037  lgsdchr  21120  2sqlem5  21140  2sqlem9  21145  2sqb  21150  pntlemp  21292  pnt3  21294  ostthlem1  21309  ostth3  21320  sizeusglecusglem1  21481  ubthlem3  22362  cdjreui  23923  cdj3i  23932  xrofsup  24114  xrge0tsmsd  24211  qqhval2  24354  mbfmco2  24603  txpcon  24907  cvmlift2lem10  24987  cvmlift2lem12  24989  cvmlift3lem7  25000  cvmlift3lem8  25001  ntrivcvgmul  25219  prodmolem2  25250  prodmo  25251  br8  25368  br6  25369  br4  25370  axcontlem4  25854  axcontlem9  25859  brsegle  25990  mblfinlem2  26191  ismblfin  26193  itg2addnc  26205  tailfb  26343  isbnd2  26429  isbnd3  26430  ssbnd  26434  ispridlc  26617  ralxpmap  26679  eldioph2  26757  eldioph2b  26758  diophin  26768  diophun  26769  fphpdo  26815  irrapxlem3  26824  irrapxlem5  26826  pell1234qrne0  26853  pell1234qrreccl  26854  pell1234qrmulcl  26855  pell14qrgt0  26859  pell14qrdich  26869  pell1qrge1  26870  pell1qrgap  26874  pellqrex  26879  rmxycomplete  26917  jm2.27  27016  psgnunilem2  27333  psgneu  27344  psgnghm  27352  stoweidlem49  27712  el2wlksotot  28223  3cyclfrgra  28263  n4cyclfrgra  28266  frgrawopreg  28296  lshpkrlem6  29752  athgt  30092  3dim1  30103  3dim2  30104  lvolex3N  30174  llncvrlpln2  30193  lplncvrlvol2  30251  linepsubN  30388  lncvrelatN  30417  linepsubclN  30587
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator