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

Theorem rexlimivv 2647
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 2642 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2636 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 1621   E.wrex 2519
This theorem is referenced by:  2reu5  2948  opelxp  4707  opiota  6256  tfrlem5  6364  xpdom2  6925  1sdom  7033  unxpdomlem3  7037  unfi  7092  elfiun  7151  xpnum  7552  kmlem9  7752  nqereu  8521  distrlem5pr  8619  mulid1  8802  1re  8805  mul02  8958  cnegex  8961  recex  9368  creur  9708  creui  9709  cju  9710  elz2  10007  zaddcl  10026  qre  10288  qaddcl  10299  qnegcl  10300  qmulcl  10301  qreccl  10303  replim  11566  xpnnenOLD  12450  odd2np1  12549  qredeu  12748  opoe  12826  omoe  12827  opeo  12828  omeo  12829  pythagtriplem1  12831  pcz  12895  4sqlem1  12957  4sqlem2  12958  4sqlem4  12961  mul4sq  12963  efgmnvl  14985  efgrelexlema  15020  txuni2  17222  tx2ndc  17307  blssioo  18263  tgioo  18264  ioorf  18890  ioorinv  18893  ioorcl  18894  dyaddisj  18913  mbfid  18953  elply  19539  vmacl  20318  efvmacl  20320  vmalelog  20406  2sqlem2  20565  mul2sq  20566  2sqlem7  20571  pntibnd  20704  ostth  20750  lpni  20806  ipasslem5  21373  ipasslem11  21378  hhssnv  21801  shscli  21856  shsleji  21909  shsidmi  21923  spansncvi  22191  superpos  22894  chirredi  22934  mdsymlem6  22948  ghomgrpilem2  23365  poseq  23622  soseq  23623  axfelem18  23732  elaltxp  23884  altxpsspw  23886  funtransport  24029  funray  24138  funline  24140  ellines  24150  linethru  24151  limptlimpr2lem2  24942  intvconlem1  25070  gltpntl  25439  mzpcompact2lem  26196  isline  29095
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2523  df-rex 2524
  Copyright terms: Public domain W3C validator