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

Theorem ralrimivv 2719
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 2717 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2710 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 1715   A.wral 2628
This theorem is referenced by:  ralrimivva  2720  ralrimdvv  2722  reuind  3054  disjxiun  4122  somo  4451  soxp  6356  sorpsscmpl  6430  smoiso  6521  smo11  6523  fiint  7280  sornom  8050  axdc4lem  8228  zorn2lem6  8275  fpwwe2lem12  8410  fpwwe2lem13  8411  nqereu  8700  genpnnp  8776  receu  9560  lbreu  9851  injresinj  11087  sqrmo  11944  iscatd  13785  isfuncd  13949  lsmsubm  15174  iscmnd  15311  divsabl  15367  dprdsubg  15469  issrngd  15836  divscrng  16202  fitop  16863  tgcl  16924  topbas  16927  ppttop  16961  epttop  16963  restbas  17106  isnrm2  17303  isnrm3  17304  2ndcctbss  17398  txbas  17479  txbasval  17518  txhaus  17558  xkohaus  17564  basqtop  17619  opnfbas  17750  isfild  17766  filfi  17767  neifil  17788  fbasrn  17792  filufint  17828  rnelfmlem  17860  fmfnfmlem3  17864  fmfnfm  17866  blf  18174  blbas  18189  minveclem3b  19007  aalioulem2  19928  grpodivf  21345  isabloda  21398  ipf  21723  ocsh  22296  adjadj  22950  unopadj2  22952  hmopadj  22953  hmopbdoptHIL  23002  lnopmi  23014  adjlnop  23100  xreceu  23692  esumcocn  24056  ghomf1olem  24673  dfon2  24974  nocvxmin  25171  axcontlem9  25427  outsideofeu  25581  hilbert1.2  25605  ontopbas  25694  opnrebl2  25828  nn0prpw  25831  fness  25874  tailfb  25918  neificl  26059  metf1o  26061  crngohomfo  26222  smprngopr  26268  ispridlc  26286  prter2  26340  mzpincl  26403  mzpindd  26415  wlkdvspthlem  27754  fargshiftf1  27771  frgrawopreglem4  27870  bnj1384  28814  snatpsubN  29998  pclclN  30139  pclfinN  30148  ltrncnv  30394  cdleme24  30600  cdleme28  30621  cdleme50ltrn  30805  cdleme  30808  ltrnco  30967  cdlemk28-3  31156  diaf11N  31298  dibf11N  31410  dihlsscpre  31483  mapdpg  31955  mapdh9a  32039  mapdh9aOLDN  32040  hdmap14lem6  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550  df-ral 2633
  Copyright terms: Public domain W3C validator