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

Theorem ralrimivv 2636
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 2634 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2627 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 1686   A.wral 2545
This theorem is referenced by:  ralrimivva  2637  ralrimdvv  2639  reuind  2970  disjxiun  4022  somo  4350  soxp  6230  sorpsscmpl  6290  smoiso  6381  smo11  6383  fiint  7135  sornom  7905  axdc4lem  8083  zorn2lem6  8130  fpwwe2lem12  8265  fpwwe2lem13  8266  nqereu  8555  genpnnp  8631  receu  9415  lbreu  9706  sqrmo  11739  iscatd  13577  isfuncd  13741  lsmsubm  14966  iscmnd  15103  divsabl  15159  dprdsubg  15261  issrngd  15628  divscrng  15994  fitop  16648  tgcl  16709  topbas  16712  ppttop  16746  epttop  16748  restbas  16891  isnrm2  17088  isnrm3  17089  2ndcctbss  17183  txbas  17264  txbasval  17303  txhaus  17343  xkohaus  17349  basqtop  17404  opnfbas  17539  isfild  17555  filfi  17556  neifil  17577  fbasrn  17581  filufint  17617  rnelfmlem  17649  fmfnfmlem3  17653  fmfnfm  17655  blf  17963  blbas  17978  minveclem3b  18794  aalioulem2  19715  grpodivf  20915  isabloda  20968  ipf  21291  ocsh  21864  adjadj  22518  unopadj2  22520  hmopadj  22521  hmopbdoptHIL  22570  lnopmi  22582  adjlnop  22668  xreceu  23107  esumcocn  23450  ghomf1olem  24003  dfon2  24150  nocvxmin  24347  axcontlem9  24602  outsideofeu  24756  hilbert1.2  24780  ontopbas  24869  injsurinj  25160  cbcpcp  25173  oriso  25225  ltrooo  25415  inttop2  25526  negveud  25679  negveudr  25680  tcnvec  25701  dualded  25794  dualcat2  25795  idfisf  25852  setiscat  25990  opnrebl2  26247  nn0prpw  26250  fness  26293  tailfb  26337  neificl  26478  metf1o  26480  crngohomfo  26642  smprngopr  26688  ispridlc  26706  prter2  26760  mzpincl  26823  mzpindd  26835  bnj1384  29135  snatpsubN  30012  pclclN  30153  pclfinN  30162  ltrncnv  30408  cdleme24  30614  cdleme28  30635  cdleme50ltrn  30819  cdleme  30822  ltrnco  30981  cdlemk28-3  31170  diaf11N  31312  dibf11N  31424  dihlsscpre  31497  mapdpg  31969  mapdh9a  32053  mapdh9aOLDN  32054  hdmap14lem6  32139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator