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

Theorem ralrimivv 2596
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 2594 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2587 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 2509
This theorem is referenced by:  ralrimivva  2597  ralrimdvv  2599  reuind  2903  disjxiun  3917  somo  4241  soxp  6080  sorpsscmpl  6140  smoiso  6265  smo11  6267  fiint  7018  sornom  7787  axdc4lem  7965  zorn2lem6  8012  fpwwe2lem12  8143  fpwwe2lem13  8144  nqereu  8433  genpnnp  8509  receu  9293  lbreu  9584  iscatd  13419  isfuncd  13583  lsmsubm  14799  iscmnd  14936  divsabl  14992  dprdsubg  15094  issrngd  15461  divscrng  15824  fitop  16478  tgcl  16539  topbas  16542  ppttop  16576  epttop  16578  restbas  16721  isnrm2  16918  isnrm3  16919  2ndcctbss  17013  txbas  17094  txbasval  17133  txhaus  17173  xkohaus  17179  basqtop  17234  opnfbas  17369  isfild  17385  filfi  17386  neifil  17407  fbasrn  17411  filufint  17447  rnelfmlem  17479  fmfnfmlem3  17483  fmfnfm  17485  blf  17793  blbas  17808  minveclem3b  18624  aalioulem2  19545  grpodivf  20743  isabloda  20796  ipf  21119  ocsh  21692  adjadj  22346  unopadj2  22348  hmopadj  22349  hmopbdoptHIL  22398  lnopmi  22410  adjlnop  22496  ghomf1olem  23172  dfon2  23316  nocvxmin  23513  axfelem14  23527  axcontlem9  23774  outsideofeu  23928  hilbert1.2  23952  ontopbas  24041  injsurinj  24315  cbcpcp  24328  oriso  24380  ltrooo  24570  inttop2  24681  negveud  24834  negveudr  24835  tcnvec  24856  dualded  24949  dualcat2  24950  idfisf  25007  setiscat  25145  opnrebl2  25402  nn0prpw  25405  fness  25448  tailfb  25492  neificl  25633  metf1o  25635  crngohomfo  25797  smprngopr  25843  ispridlc  25861  prter2  25915  mzpincl  25978  mzpindd  25990  bnj1384  27751  snatpsubN  28740  pclclN  28881  pclfinN  28890  ltrncnv  29136  cdleme24  29342  cdleme28  29363  cdleme50ltrn  29547  cdleme  29550  ltrnco  29709  cdlemk28-3  29898  diaf11N  30040  dibf11N  30152  dihlsscpre  30225  mapdpg  30697  mapdh9a  30781  mapdh9aOLDN  30782  hdmap14lem6  30867
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 2513
  Copyright terms: Public domain W3C validator