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

Theorem ralrimivv 2634
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
Hypothesis
Ref Expression
ralrimivv.1  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
Assertion
Ref Expression
ralrimivv  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Distinct variable groups:    x, y, ph    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem ralrimivv
StepHypRef Expression
1 ralrimivv.1 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
21exp3a 425 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ps ) ) )
32ralrimdv 2632 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2625 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralrimivva  2635  ralrimdvv  2637  reuind  2968  disjxiun  4020  somo  4348  soxp  6228  sorpsscmpl  6288  smoiso  6379  smo11  6381  fiint  7133  sornom  7903  axdc4lem  8081  zorn2lem6  8128  fpwwe2lem12  8263  fpwwe2lem13  8264  nqereu  8553  genpnnp  8629  receu  9413  lbreu  9704  sqrmo  11737  iscatd  13575  isfuncd  13739  lsmsubm  14964  iscmnd  15101  divsabl  15157  dprdsubg  15259  issrngd  15626  divscrng  15992  fitop  16646  tgcl  16707  topbas  16710  ppttop  16744  epttop  16746  restbas  16889  isnrm2  17086  isnrm3  17087  2ndcctbss  17181  txbas  17262  txbasval  17301  txhaus  17341  xkohaus  17347  basqtop  17402  opnfbas  17537  isfild  17553  filfi  17554  neifil  17575  fbasrn  17579  filufint  17615  rnelfmlem  17647  fmfnfmlem3  17651  fmfnfm  17653  blf  17961  blbas  17976  minveclem3b  18792  aalioulem2  19713  grpodivf  20913  isabloda  20966  ipf  21289  ocsh  21862  adjadj  22516  unopadj2  22518  hmopadj  22519  hmopbdoptHIL  22568  lnopmi  22580  adjlnop  22666  xreceu  23105  esumcocn  23448  ghomf1olem  24001  dfon2  24148  nocvxmin  24345  axcontlem9  24600  outsideofeu  24754  hilbert1.2  24778  ontopbas  24867  injsurinj  25149  cbcpcp  25162  oriso  25214  ltrooo  25404  inttop2  25515  negveud  25668  negveudr  25669  tcnvec  25690  dualded  25783  dualcat2  25784  idfisf  25841  setiscat  25979  opnrebl2  26236  nn0prpw  26239  fness  26282  tailfb  26326  neificl  26467  metf1o  26469  crngohomfo  26631  smprngopr  26677  ispridlc  26695  prter2  26749  mzpincl  26812  mzpindd  26824  bnj1384  29062  snatpsubN  29939  pclclN  30080  pclfinN  30089  ltrncnv  30335  cdleme24  30541  cdleme28  30562  cdleme50ltrn  30746  cdleme  30749  ltrnco  30908  cdlemk28-3  31097  diaf11N  31239  dibf11N  31351  dihlsscpre  31424  mapdpg  31896  mapdh9a  31980  mapdh9aOLDN  31981  hdmap14lem6  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator