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

Theorem ralrimivv 2789
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 426 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ps ) ) )
32ralrimdv 2787 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2780 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ralrimivva  2790  ralrimdvv  2792  reuind  3129  disjxiun  4201  somo  4529  ssrel2  4958  f1o2ndf1  6446  soxp  6451  sorpsscmpl  6525  smoiso  6616  smo11  6618  fiint  7375  sornom  8149  axdc4lem  8327  zorn2lem6  8373  fpwwe2lem12  8508  fpwwe2lem13  8509  nqereu  8798  genpnnp  8874  receu  9659  lbreu  9950  injresinj  11192  sqrmo  12049  iscatd  13890  isfuncd  14054  lsmsubm  15279  iscmnd  15416  divsabl  15472  dprdsubg  15574  issrngd  15941  divscrng  16303  fitop  16965  tgcl  17026  topbas  17029  ppttop  17063  epttop  17065  restbas  17214  isnrm2  17414  isnrm3  17415  2ndcctbss  17510  txbas  17591  txbasval  17630  txhaus  17671  xkohaus  17677  basqtop  17735  opnfbas  17866  isfild  17882  filfi  17883  neifil  17904  fbasrn  17908  filufint  17944  rnelfmlem  17976  fmfnfmlem3  17980  fmfnfm  17982  blfps  18428  blf  18429  blbas  18452  minveclem3b  19321  aalioulem2  20242  wlkdvspthlem  21599  grpodivf  21826  isabloda  21879  ipf  22204  ocsh  22777  adjadj  23431  unopadj2  23433  hmopadj  23434  hmopbdoptHIL  23483  lnopmi  23495  adjlnop  23581  xreceu  24160  esumcocn  24462  ghomf1olem  25097  dfon2  25411  nocvxmin  25638  axcontlem9  25903  outsideofeu  26057  hilbert1.2  26081  ontopbas  26170  opnrebl2  26315  nn0prpw  26317  fness  26353  tailfb  26397  neificl  26450  metf1o  26452  crngohomfo  26607  smprngopr  26653  ispridlc  26671  prter2  26721  mzpincl  26782  mzpindd  26794  frgrawopreglem4  28373  iunconlem2  28984  bnj1384  29338  snatpsubN  30484  pclclN  30625  pclfinN  30634  ltrncnv  30880  cdleme24  31086  cdleme28  31107  cdleme50ltrn  31291  cdleme  31294  ltrnco  31453  cdlemk28-3  31642  diaf11N  31784  dibf11N  31896  dihlsscpre  31969  mapdpg  32441  mapdh9a  32525  mapdh9aOLDN  32526  hdmap14lem6  32611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator