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

Theorem ralrimivv 2609
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 2607 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2600 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 2518
This theorem is referenced by:  ralrimivva  2610  ralrimdvv  2612  reuind  2943  disjxiun  3994  somo  4320  soxp  6162  sorpsscmpl  6222  smoiso  6347  smo11  6349  fiint  7101  sornom  7871  axdc4lem  8049  zorn2lem6  8096  fpwwe2lem12  8231  fpwwe2lem13  8232  nqereu  8521  genpnnp  8597  receu  9381  lbreu  9672  sqrmo  11703  iscatd  13538  isfuncd  13702  lsmsubm  14927  iscmnd  15064  divsabl  15120  dprdsubg  15222  issrngd  15589  divscrng  15955  fitop  16609  tgcl  16670  topbas  16673  ppttop  16707  epttop  16709  restbas  16852  isnrm2  17049  isnrm3  17050  2ndcctbss  17144  txbas  17225  txbasval  17264  txhaus  17304  xkohaus  17310  basqtop  17365  opnfbas  17500  isfild  17516  filfi  17517  neifil  17538  fbasrn  17542  filufint  17578  rnelfmlem  17610  fmfnfmlem3  17614  fmfnfm  17616  blf  17924  blbas  17939  minveclem3b  18755  aalioulem2  19676  grpodivf  20874  isabloda  20927  ipf  21250  ocsh  21823  adjadj  22477  unopadj2  22479  hmopadj  22480  hmopbdoptHIL  22529  lnopmi  22541  adjlnop  22627  ghomf1olem  23374  dfon2  23518  nocvxmin  23715  axfelem14  23729  axcontlem9  23976  outsideofeu  24130  hilbert1.2  24154  ontopbas  24243  injsurinj  24517  cbcpcp  24530  oriso  24582  ltrooo  24772  inttop2  24883  negveud  25036  negveudr  25037  tcnvec  25058  dualded  25151  dualcat2  25152  idfisf  25209  setiscat  25347  opnrebl2  25604  nn0prpw  25607  fness  25650  tailfb  25694  neificl  25835  metf1o  25837  crngohomfo  25999  smprngopr  26045  ispridlc  26063  prter2  26117  mzpincl  26180  mzpindd  26192  bnj1384  28194  snatpsubN  29189  pclclN  29330  pclfinN  29339  ltrncnv  29585  cdleme24  29791  cdleme28  29812  cdleme50ltrn  29996  cdleme  29999  ltrnco  30158  cdlemk28-3  30347  diaf11N  30489  dibf11N  30601  dihlsscpre  30674  mapdpg  31146  mapdh9a  31230  mapdh9aOLDN  31231  hdmap14lem6  31316
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 2523
  Copyright terms: Public domain W3C validator