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

Theorem rexlimivv 2673
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimivv  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Distinct variable groups:    x, y, ps    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( ph  ->  ps ) )
21rexlimdva 2668 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2662 1  |-  ( E. x  e.  A  E. y  e.  B  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1688   E.wrex 2545
This theorem is referenced by:  2reu5  2974  opelxp  4718  opiota  6283  tfrlem5  6391  xpdom2  6952  1sdom  7060  unxpdomlem3  7064  unfi  7119  elfiun  7178  xpnum  7579  kmlem9  7779  nqereu  8548  distrlem5pr  8646  mulid1  8830  1re  8832  mul02  8985  cnegex  8988  recex  9395  creur  9735  creui  9736  cju  9737  elz2  10035  zaddcl  10054  qre  10316  qaddcl  10327  qnegcl  10328  qmulcl  10329  qreccl  10331  replim  11595  xpnnenOLD  12482  odd2np1  12581  qredeu  12780  opoe  12858  omoe  12859  opeo  12860  omeo  12861  pythagtriplem1  12863  pcz  12927  4sqlem1  12989  4sqlem2  12990  4sqlem4  12993  mul4sq  12995  efgmnvl  15017  efgrelexlema  15052  txuni2  17254  tx2ndc  17339  blssioo  18295  tgioo  18296  ioorf  18922  ioorinv  18925  ioorcl  18926  dyaddisj  18945  mbfid  18985  elply  19571  vmacl  20350  efvmacl  20352  vmalelog  20438  2sqlem2  20597  mul2sq  20598  2sqlem7  20603  pntibnd  20736  ostth  20782  lpni  20838  ipasslem5  21405  ipasslem11  21410  hhssnv  21833  shscli  21888  shsleji  21941  shsidmi  21955  spansncvi  22223  superpos  22926  chirredi  22966  mdsymlem6  22980  ghomgrpilem2  23397  poseq  23654  soseq  23655  axfelem18  23764  elaltxp  23916  altxpsspw  23918  funtransport  24061  funray  24170  funline  24172  ellines  24182  linethru  24183  limptlimpr2lem2  24974  intvconlem1  25102  gltpntl  25471  mzpcompact2lem  26228  2reu4  27347  isline  29195
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-nf 1537  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator