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

Theorem ralrimivv 2710
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 2708 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2701 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 1710   A.wral 2619
This theorem is referenced by:  ralrimivva  2711  ralrimdvv  2713  reuind  3044  disjxiun  4099  somo  4427  soxp  6312  sorpsscmpl  6372  smoiso  6463  smo11  6465  fiint  7220  sornom  7990  axdc4lem  8168  zorn2lem6  8215  fpwwe2lem12  8350  fpwwe2lem13  8351  nqereu  8640  genpnnp  8716  receu  9500  lbreu  9791  sqrmo  11827  iscatd  13668  isfuncd  13832  lsmsubm  15057  iscmnd  15194  divsabl  15250  dprdsubg  15352  issrngd  15719  divscrng  16085  fitop  16746  tgcl  16807  topbas  16810  ppttop  16844  epttop  16846  restbas  16989  isnrm2  17186  isnrm3  17187  2ndcctbss  17281  txbas  17362  txbasval  17401  txhaus  17441  xkohaus  17447  basqtop  17502  opnfbas  17633  isfild  17649  filfi  17650  neifil  17671  fbasrn  17675  filufint  17711  rnelfmlem  17743  fmfnfmlem3  17747  fmfnfm  17749  blf  18057  blbas  18072  minveclem3b  18890  aalioulem2  19811  grpodivf  21019  isabloda  21072  ipf  21397  ocsh  21970  adjadj  22624  unopadj2  22626  hmopadj  22627  hmopbdoptHIL  22676  lnopmi  22688  adjlnop  22774  xreceu  23372  esumcocn  23736  ghomf1olem  24405  dfon2  24706  nocvxmin  24903  axcontlem9  25159  outsideofeu  25313  hilbert1.2  25337  ontopbas  25426  opnrebl2  25560  nn0prpw  25563  fness  25606  tailfb  25650  neificl  25791  metf1o  25793  crngohomfo  25954  smprngopr  26000  ispridlc  26018  prter2  26072  mzpincl  26135  mzpindd  26147  injresinj  27460  wlkdvspthlem  27726  fargshiftf1  27743  frgrawopreglem4  27863  bnj1384  28807  snatpsubN  29991  pclclN  30132  pclfinN  30141  ltrncnv  30387  cdleme24  30593  cdleme28  30614  cdleme50ltrn  30798  cdleme  30801  ltrnco  30960  cdlemk28-3  31149  diaf11N  31291  dibf11N  31403  dihlsscpre  31476  mapdpg  31948  mapdh9a  32032  mapdh9aOLDN  32033  hdmap14lem6  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2624
  Copyright terms: Public domain W3C validator