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

Theorem ralrimivv 2635
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 2633 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2626 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 1685   A.wral 2544
This theorem is referenced by:  ralrimivva  2636  ralrimdvv  2638  reuind  2969  disjxiun  4021  somo  4347  soxp  6190  sorpsscmpl  6250  smoiso  6375  smo11  6377  fiint  7129  sornom  7899  axdc4lem  8077  zorn2lem6  8124  fpwwe2lem12  8259  fpwwe2lem13  8260  nqereu  8549  genpnnp  8625  receu  9409  lbreu  9700  sqrmo  11733  iscatd  13571  isfuncd  13735  lsmsubm  14960  iscmnd  15097  divsabl  15153  dprdsubg  15255  issrngd  15622  divscrng  15988  fitop  16642  tgcl  16703  topbas  16706  ppttop  16740  epttop  16742  restbas  16885  isnrm2  17082  isnrm3  17083  2ndcctbss  17177  txbas  17258  txbasval  17297  txhaus  17337  xkohaus  17343  basqtop  17398  opnfbas  17533  isfild  17549  filfi  17550  neifil  17571  fbasrn  17575  filufint  17611  rnelfmlem  17643  fmfnfmlem3  17647  fmfnfm  17649  blf  17957  blbas  17972  minveclem3b  18788  aalioulem2  19709  grpodivf  20907  isabloda  20960  ipf  21283  ocsh  21858  adjadj  22512  unopadj2  22514  hmopadj  22515  hmopbdoptHIL  22564  lnopmi  22576  adjlnop  22662  ghomf1olem  23408  dfon2  23552  nocvxmin  23749  axfelem14  23763  axcontlem9  24010  outsideofeu  24164  hilbert1.2  24188  ontopbas  24277  injsurinj  24560  cbcpcp  24573  oriso  24625  ltrooo  24815  inttop2  24926  negveud  25079  negveudr  25080  tcnvec  25101  dualded  25194  dualcat2  25195  idfisf  25252  setiscat  25390  opnrebl2  25647  nn0prpw  25650  fness  25693  tailfb  25737  neificl  25878  metf1o  25880  crngohomfo  26042  smprngopr  26088  ispridlc  26106  prter2  26160  mzpincl  26223  mzpindd  26235  bnj1384  28341  snatpsubN  29218  pclclN  29359  pclfinN  29368  ltrncnv  29614  cdleme24  29820  cdleme28  29841  cdleme50ltrn  30025  cdleme  30028  ltrnco  30187  cdlemk28-3  30376  diaf11N  30518  dibf11N  30630  dihlsscpre  30703  mapdpg  31175  mapdh9a  31259  mapdh9aOLDN  31260  hdmap14lem6  31345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2549
  Copyright terms: Public domain W3C validator