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

Theorem ralrimivv 2605
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 427 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ps ) ) )
32ralrimdv 2603 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2596 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   A.wral 2516
This theorem is referenced by:  ralrimivva  2606  ralrimdvv  2608  reuind  2917  disjxiun  3960  somo  4285  soxp  6127  sorpsscmpl  6187  smoiso  6312  smo11  6314  fiint  7066  sornom  7836  axdc4lem  8014  zorn2lem6  8061  fpwwe2lem12  8196  fpwwe2lem13  8197  nqereu  8486  genpnnp  8562  receu  9346  lbreu  9637  iscatd  13502  isfuncd  13666  lsmsubm  14891  iscmnd  15028  divsabl  15084  dprdsubg  15186  issrngd  15553  divscrng  15919  fitop  16573  tgcl  16634  topbas  16637  ppttop  16671  epttop  16673  restbas  16816  isnrm2  17013  isnrm3  17014  2ndcctbss  17108  txbas  17189  txbasval  17228  txhaus  17268  xkohaus  17274  basqtop  17329  opnfbas  17464  isfild  17480  filfi  17481  neifil  17502  fbasrn  17506  filufint  17542  rnelfmlem  17574  fmfnfmlem3  17578  fmfnfm  17580  blf  17888  blbas  17903  minveclem3b  18719  aalioulem2  19640  grpodivf  20838  isabloda  20891  ipf  21214  ocsh  21787  adjadj  22441  unopadj2  22443  hmopadj  22444  hmopbdoptHIL  22493  lnopmi  22505  adjlnop  22591  ghomf1olem  23338  dfon2  23482  nocvxmin  23679  axfelem14  23693  axcontlem9  23940  outsideofeu  24094  hilbert1.2  24118  ontopbas  24207  injsurinj  24481  cbcpcp  24494  oriso  24546  ltrooo  24736  inttop2  24847  negveud  25000  negveudr  25001  tcnvec  25022  dualded  25115  dualcat2  25116  idfisf  25173  setiscat  25311  opnrebl2  25568  nn0prpw  25571  fness  25614  tailfb  25658  neificl  25799  metf1o  25801  crngohomfo  25963  smprngopr  26009  ispridlc  26027  prter2  26081  mzpincl  26144  mzpindd  26156  bnj1384  28074  snatpsubN  29069  pclclN  29210  pclfinN  29219  ltrncnv  29465  cdleme24  29671  cdleme28  29692  cdleme50ltrn  29876  cdleme  29879  ltrnco  30038  cdlemk28-3  30227  diaf11N  30369  dibf11N  30481  dihlsscpre  30554  mapdpg  31026  mapdh9a  31110  mapdh9aOLDN  31111  hdmap14lem6  31196
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2520
  Copyright terms: Public domain W3C validator