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

Theorem ralrimivv 2761
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 426 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ps ) ) )
32ralrimdv 2759 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2752 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   A.wral 2670
This theorem is referenced by:  ralrimivva  2762  ralrimdvv  2764  reuind  3101  disjxiun  4173  somo  4501  ssrel2  4929  f1o2ndf1  6417  soxp  6422  sorpsscmpl  6496  smoiso  6587  smo11  6589  fiint  7346  sornom  8117  axdc4lem  8295  zorn2lem6  8341  fpwwe2lem12  8476  fpwwe2lem13  8477  nqereu  8766  genpnnp  8842  receu  9627  lbreu  9918  injresinj  11159  sqrmo  12016  iscatd  13857  isfuncd  14021  lsmsubm  15246  iscmnd  15383  divsabl  15439  dprdsubg  15541  issrngd  15908  divscrng  16270  fitop  16932  tgcl  16993  topbas  16996  ppttop  17030  epttop  17032  restbas  17180  isnrm2  17380  isnrm3  17381  2ndcctbss  17475  txbas  17556  txbasval  17595  txhaus  17636  xkohaus  17642  basqtop  17700  opnfbas  17831  isfild  17847  filfi  17848  neifil  17869  fbasrn  17873  filufint  17909  rnelfmlem  17941  fmfnfmlem3  17945  fmfnfm  17947  blfps  18393  blf  18394  blbas  18417  minveclem3b  19286  aalioulem2  20207  wlkdvspthlem  21564  grpodivf  21791  isabloda  21844  ipf  22169  ocsh  22742  adjadj  23396  unopadj2  23398  hmopadj  23399  hmopbdoptHIL  23448  lnopmi  23460  adjlnop  23546  xreceu  24125  esumcocn  24427  ghomf1olem  25062  dfon2  25366  nocvxmin  25563  axcontlem9  25819  outsideofeu  25973  hilbert1.2  25997  ontopbas  26086  opnrebl2  26218  nn0prpw  26220  fness  26256  tailfb  26300  neificl  26353  metf1o  26355  crngohomfo  26510  smprngopr  26556  ispridlc  26574  prter2  26624  mzpincl  26685  mzpindd  26697  frgrawopreglem4  28154  bnj1384  29111  snatpsubN  30236  pclclN  30377  pclfinN  30386  ltrncnv  30632  cdleme24  30838  cdleme28  30859  cdleme50ltrn  31043  cdleme  31046  ltrnco  31205  cdlemk28-3  31394  diaf11N  31536  dibf11N  31648  dihlsscpre  31721  mapdpg  32193  mapdh9a  32277  mapdh9aOLDN  32278  hdmap14lem6  32363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675
  Copyright terms: Public domain W3C validator