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

Theorem rexlimdvv 2644
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 428 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2637 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2638 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  rexlimdvva  2645  f1oiso2  5748  omeu  6516  xpdom2  6890  elfiun  7116  rankxplim3  7484  brdom6disj  8090  fpwwe2lem12  8196  tskxpss  8327  genpss  8561  genpcd  8563  genpnmax  8564  distrlem1pr  8582  distrlem5pr  8584  ltexprlem6  8598  reclem4pr  8607  supmullem1  9653  supmullem2  9654  qaddcl  10264  qmulcl  10266  sqrlem6  11663  caubnd  11772  summo  12120  xpnnenOLD  12415  bezoutlem3  12646  bezoutlem4  12647  dvdsgcd  12649  gcddiv  12655  pceu  12826  pcqcl  12836  lspfixed  15808  lspexch  15809  lsmcv  15821  lspsolvlem  15822  hausnei2  17008  uncmp  17057  txcnp  17241  tx1stc  17271  fbasrn  17506  rnelfmlem  17574  blss  17899  tgqioo  18233  ovolunlem2  18784  pjhthmo  21806  shmodsi  21893  pjpjpre  21923  chscllem4  22162  sumdmdlem  22923  cdj3lem2a  22941  cdj3lem2b  22942  cdj3lem3a  22944  fprb  23463  axfelem19  23698  ax5seg  23906  axpasch  23909  axeuclid  23931  btwndiff  23990  btwnconn1lem13  24062  btwnconn1lem14  24063  brsegle  24071  segletr  24077  segleantisym  24078  nn0prpwlem  25570  heibor1lem  25865  crngohomfo  25963  mzpcompact2lem  26161  pellex  26252  stoweidlem49  27098  lsmsat  28328  3dim1  28786  3dim3  28788  1cvratex  28792  atcvrlln2  28838  atcvrlln  28839  lplnnlelln  28862  llncvrlpln2  28876  lplnexllnN  28883  2llnjN  28886  lvolnlelln  28903  lvolnlelpln  28904  lplncvrlvol2  28934  2lplnj  28939  lneq2at  29097  lnatexN  29098  lncvrat  29101  lncmp  29102  paddasslem15  29153  paddasslem16  29154  pmodlem2  29166  pmapjoin  29171  llnexchb2  29188  lhp2lt  29320  cdlemf  29882  cdlemg1cex  29907  cdlemg2ce  29911  cdlemn11pre  30530  dihord2pre  30545  dihord4  30578  dihmeetlem20N  30646  mapdpglem24  31024  mapdpglem32  31025  baerlem3lem2  31030  baerlem5alem2  31031  baerlem5blem2  31032  hdmapglem7  31252
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