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

Theorem rexlimivv 2634
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 2629 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2623 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 2510
This theorem is referenced by:  opelxp  4626  opiota  6174  tfrlem5  6282  xpdom2  6842  1sdom  6950  unxpdomlem3  6954  unfi  7009  elfiun  7067  xpnum  7468  kmlem9  7668  nqereu  8433  distrlem5pr  8531  mulid1  8714  1re  8717  mul02  8870  cnegex  8873  recex  9280  creur  9620  creui  9621  cju  9622  elz2  9919  zaddcl  9938  qre  10200  qaddcl  10211  qnegcl  10212  qmulcl  10213  qreccl  10215  replim  11478  xpnnenOLD  12362  odd2np1  12461  qredeu  12660  opoe  12738  omoe  12739  opeo  12740  omeo  12741  pythagtriplem1  12743  pcz  12807  4sqlem1  12869  4sqlem2  12870  4sqlem4  12873  mul4sq  12875  efgmnvl  14858  efgrelexlema  14893  txuni2  17092  tx2ndc  17177  blssioo  18133  tgioo  18134  ioorf  18760  ioorinv  18763  ioorcl  18764  dyaddisj  18783  mbfid  18823  elply  19409  vmacl  20188  efvmacl  20190  vmalelog  20276  2sqlem2  20435  mul2sq  20436  2sqlem7  20441  pntibnd  20574  ostth  20620  lpni  20676  ipasslem5  21243  ipasslem11  21248  hhssnv  21671  shscli  21726  shsleji  21779  shsidmi  21793  spansncvi  22079  superpos  22764  chirredi  22804  mdsymlem6  22818  ghomgrpilem2  23164  poseq  23421  soseq  23422  axfelem18  23531  elaltxp  23683  altxpsspw  23685  funtransport  23828  funray  23937  funline  23939  ellines  23949  linethru  23950  limptlimpr2lem2  24741  intvconlem1  24869  gltpntl  25238  mzpcompact2lem  25995  isline  28729
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator