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

Theorem ralrimivv 2797
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 2795 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2788 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 2705
This theorem is referenced by:  ralrimivva  2798  ralrimdvv  2800  reuind  3137  disjxiun  4209  somo  4537  ssrel2  4966  f1o2ndf1  6454  soxp  6459  sorpsscmpl  6533  smoiso  6624  smo11  6626  fiint  7383  sornom  8157  axdc4lem  8335  zorn2lem6  8381  fpwwe2lem12  8516  fpwwe2lem13  8517  nqereu  8806  genpnnp  8882  receu  9667  lbreu  9958  injresinj  11200  sqrmo  12057  iscatd  13898  isfuncd  14062  lsmsubm  15287  iscmnd  15424  divsabl  15480  dprdsubg  15582  issrngd  15949  divscrng  16311  fitop  16973  tgcl  17034  topbas  17037  ppttop  17071  epttop  17073  restbas  17222  isnrm2  17422  isnrm3  17423  2ndcctbss  17518  txbas  17599  txbasval  17638  txhaus  17679  xkohaus  17685  basqtop  17743  opnfbas  17874  isfild  17890  filfi  17891  neifil  17912  fbasrn  17916  filufint  17952  rnelfmlem  17984  fmfnfmlem3  17988  fmfnfm  17990  blfps  18436  blf  18437  blbas  18460  minveclem3b  19329  aalioulem2  20250  wlkdvspthlem  21607  grpodivf  21834  isabloda  21887  ipf  22212  ocsh  22785  adjadj  23439  unopadj2  23441  hmopadj  23442  hmopbdoptHIL  23491  lnopmi  23503  adjlnop  23589  xreceu  24168  esumcocn  24470  ghomf1olem  25105  dfon2  25419  nocvxmin  25646  axcontlem9  25911  outsideofeu  26065  hilbert1.2  26089  ontopbas  26178  opnrebl2  26324  nn0prpw  26326  fness  26362  tailfb  26406  neificl  26459  metf1o  26461  crngohomfo  26616  smprngopr  26662  ispridlc  26680  prter2  26730  mzpincl  26791  mzpindd  26803  frgrawopreglem4  28436  iunconlem2  29047  bnj1384  29401  snatpsubN  30547  pclclN  30688  pclfinN  30697  ltrncnv  30943  cdleme24  31149  cdleme28  31170  cdleme50ltrn  31354  cdleme  31357  ltrnco  31516  cdlemk28-3  31705  diaf11N  31847  dibf11N  31959  dihlsscpre  32032  mapdpg  32504  mapdh9a  32588  mapdh9aOLDN  32589  hdmap14lem6  32674
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 2710
  Copyright terms: Public domain W3C validator