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

Theorem rexlimdvva 2687
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 423 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
32rexlimdvv 2686 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  disjxiun  4036  eroveu  6769  eroprf  6772  unxpdomlem3  7085  finsschain  7178  dffi3  7200  sornom  7919  genpv  8639  genpdm  8642  1re  8853  cnegex  9009  zaddcl  10075  rexanre  11846  o1lo1  12027  lo1resb  12054  o1resb  12056  rlimcn2  12080  climcn2  12082  o1of2  12102  o1rlimmul  12108  lo1add  12116  lo1mul  12117  summo  12206  o1fsum  12287  dvds2lem  12557  bezoutlem4  12736  dvdsmulgcd  12749  pcqmul  12922  pcneg  12942  pcadd  12953  4sqlem1  13011  4sqlem2  13012  4sqlem4  13015  mul4sq  13017  4sqlem12  13019  4sqlem13  13020  4sqlem18  13025  vdwmc2  13042  vdwlem7  13050  vdwlem9  13052  vdwlem10  13053  vdwlem11  13054  ramlb  13082  ramub1lem2  13090  imasaddfnlem  13446  imasmnd2  14425  imasgrp2  14626  gaorber  14778  lsmsubm  14980  lsmsubg  14981  lsmmod  15000  lsmdisj2  15007  pj1eu  15021  efgtlen  15051  efgredlem  15072  efgredeu  15077  efgcpbllemb  15080  frgpuptinv  15096  frgpup3lem  15102  divsabl  15173  frgpnabllem1  15177  frgpnabl  15179  cygabl  15193  dprdsubg  15275  ablfacrp  15317  pgpfac1lem3  15328  imasrng  15418  dvdsrtr  15450  lss1d  15736  lsmcl  15852  lsmelval2  15854  lbsextlem2  15928  isnzr2  16031  qsssubdrg  16447  znfld  16530  cygznlem3  16539  lsmcss  16608  restbas  16905  ordtbas2  16937  ordtbas  16938  cnhaus  17098  cldllycmp  17237  txbas  17278  ptbasin  17288  txcls  17315  xkoccn  17329  txindis  17344  txlly  17346  txnlly  17347  pthaus  17348  ptrescn  17349  txhaus  17357  tx1stc  17360  txkgen  17362  xkohaus  17363  xkoptsub  17364  xkopt  17365  xkoco1cn  17367  xkoco2cn  17368  xkoinjcn  17397  fmfnfmlem3  17667  fmfnfmlem4  17668  hausflimi  17691  hauspwpwf1  17698  txflf  17717  divstgplem  17819  blin2  17991  prdsxmslem2  18091  xrge0tsms  18355  addcnlem  18384  minveclem3b  18808  pmltpc  18826  evthicc2  18836  dyaddisj  18967  ismbfd  19011  mbfimaopnlem  19026  rolle  19353  dvcnvrelem1  19380  dvcvx  19383  itgsubst  19412  plyf  19596  plypf1  19610  plyadd  19615  plymul  19616  coeeu  19623  dgrlem  19627  coeid  19636  aalioulem6  19733  o1cxp  20285  dchrptlem2  20520  lgsdchr  20603  2sqlem5  20623  2sqlem9  20628  2sqb  20633  pntlemp  20775  pnt3  20777  ostthlem1  20792  ostth3  20803  ubthlem3  21467  cdjreui  23028  cdj3i  23037  xrge0tsmsd  23397  mbfmco2  23585  txpcon  23778  cvmlift2lem10  23858  cvmlift2lem12  23860  cvmlift3lem7  23871  cvmlift3lem8  23872  prodmolem2  24158  prodmo  24159  br8  24184  br6  24185  br4  24186  axcontlem4  24667  axcontlem9  24672  brsegle  24803  itg2addnc  25005  uninqs  25142  repcpwti  25264  tailfb  26429  isbnd2  26610  isbnd3  26611  ssbnd  26615  ispridlc  26798  ralxpmap  26864  eldioph2  26944  eldioph2b  26945  diophin  26955  diophun  26956  fphpdo  27003  irrapxlem3  27012  irrapxlem5  27014  pell1234qrne0  27041  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrgt0  27047  pell14qrdich  27057  pell1qrge1  27058  pell1qrgap  27062  pellqrex  27067  rmxycomplete  27105  jm2.27  27204  psgnunilem2  27521  psgneu  27532  psgnghm  27540  3cyclfrgra  28437  n4cyclfrgra  28440  lshpkrlem6  29927  athgt  30267  3dim1  30278  3dim2  30279  lvolex3N  30349  llncvrlpln2  30368  lplncvrlvol2  30426  linepsubN  30563  lncvrelatN  30592  linepsubclN  30762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator