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

Theorem rexlimivv 2643
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 2638 . 2  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  ps ) )
32rexlimiv 2632 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 2517
This theorem is referenced by:  opelxp  4672  opiota  6221  tfrlem5  6329  xpdom2  6890  1sdom  6998  unxpdomlem3  7002  unfi  7057  elfiun  7116  xpnum  7517  kmlem9  7717  nqereu  8486  distrlem5pr  8584  mulid1  8767  1re  8770  mul02  8923  cnegex  8926  recex  9333  creur  9673  creui  9674  cju  9675  elz2  9972  zaddcl  9991  qre  10253  qaddcl  10264  qnegcl  10265  qmulcl  10266  qreccl  10268  replim  11531  xpnnenOLD  12415  odd2np1  12514  qredeu  12713  opoe  12791  omoe  12792  opeo  12793  omeo  12794  pythagtriplem1  12796  pcz  12860  4sqlem1  12922  4sqlem2  12923  4sqlem4  12926  mul4sq  12928  efgmnvl  14950  efgrelexlema  14985  txuni2  17187  tx2ndc  17272  blssioo  18228  tgioo  18229  ioorf  18855  ioorinv  18858  ioorcl  18859  dyaddisj  18878  mbfid  18918  elply  19504  vmacl  20283  efvmacl  20285  vmalelog  20371  2sqlem2  20530  mul2sq  20531  2sqlem7  20536  pntibnd  20669  ostth  20715  lpni  20771  ipasslem5  21338  ipasslem11  21343  hhssnv  21766  shscli  21821  shsleji  21874  shsidmi  21888  spansncvi  22174  superpos  22859  chirredi  22899  mdsymlem6  22913  ghomgrpilem2  23330  poseq  23587  soseq  23588  axfelem18  23697  elaltxp  23849  altxpsspw  23851  funtransport  23994  funray  24103  funline  24105  ellines  24115  linethru  24116  limptlimpr2lem2  24907  intvconlem1  25035  gltpntl  25404  mzpcompact2lem  26161  isline  29058
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 2520  df-rex 2521
  Copyright terms: Public domain W3C validator