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

Theorem rexlimdvv 2796
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
rexlimdvv.1  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimdvv  |-  ( 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 rexlimdvv
StepHypRef Expression
1 rexlimdvv.1 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
21expdimp 427 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2789 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2790 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  rexlimdvva  2797  f1oiso2  6031  omeu  6787  xpdom2  7162  elfiun  7393  rankxplim3  7761  brdom6disj  8366  fpwwe2lem12  8472  tskxpss  8603  genpss  8837  genpcd  8839  genpnmax  8840  distrlem1pr  8858  distrlem5pr  8860  ltexprlem6  8874  reclem4pr  8883  supmullem1  9930  supmullem2  9931  qaddcl  10546  qmulcl  10548  sqrlem6  12008  caubnd  12117  summo  12466  xpnnenOLD  12764  bezoutlem3  12995  bezoutlem4  12996  dvdsgcd  12998  gcddiv  13004  pceu  13175  pcqcl  13185  lspfixed  16155  lspexch  16156  lsmcv  16168  lspsolvlem  16169  hausnei2  17371  uncmp  17420  txcnp  17605  tx1stc  17635  fbasrn  17869  rnelfmlem  17937  blssps  18407  blss  18408  tgqioo  18784  ovolunlem2  19347  pjhthmo  22757  shmodsi  22844  pjpjpre  22874  chscllem4  23095  sumdmdlem  23874  cdj3lem2a  23892  cdj3lem2b  23893  cdj3lem3a  23895  dya2iocnrect  24584  fprb  25343  ax5seg  25781  axpasch  25784  axeuclid  25806  btwndiff  25865  btwnconn1lem13  25937  btwnconn1lem14  25938  brsegle  25946  segletr  25952  segleantisym  25953  supadd  26138  ismblfin  26146  nn0prpwlem  26215  heibor1lem  26408  crngohomfo  26506  mzpcompact2lem  26698  pellex  26788  frgrawopreg  28152  lsmsat  29491  3dim1  29949  3dim3  29951  1cvratex  29955  atcvrlln2  30001  atcvrlln  30002  lplnnlelln  30025  llncvrlpln2  30039  lplnexllnN  30046  2llnjN  30049  lvolnlelln  30066  lvolnlelpln  30067  lplncvrlvol2  30097  2lplnj  30102  lneq2at  30260  lnatexN  30261  lncvrat  30264  lncmp  30265  paddasslem15  30316  paddasslem16  30317  pmodlem2  30329  pmapjoin  30334  llnexchb2  30351  lhp2lt  30483  cdlemf  31045  cdlemg1cex  31070  cdlemg2ce  31074  cdlemn11pre  31693  dihord2pre  31708  dihord4  31741  dihmeetlem20N  31809  mapdpglem24  32187  mapdpglem32  32188  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmapglem7  32415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator