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

Theorem ralrimivv 2757
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 2755 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2748 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 2666
This theorem is referenced by:  ralrimivva  2758  ralrimdvv  2760  reuind  3097  disjxiun  4169  somo  4497  ssrel2  4925  f1o2ndf1  6413  soxp  6418  sorpsscmpl  6492  smoiso  6583  smo11  6585  fiint  7342  sornom  8113  axdc4lem  8291  zorn2lem6  8337  fpwwe2lem12  8472  fpwwe2lem13  8473  nqereu  8762  genpnnp  8838  receu  9623  lbreu  9914  injresinj  11155  sqrmo  12012  iscatd  13853  isfuncd  14017  lsmsubm  15242  iscmnd  15379  divsabl  15435  dprdsubg  15537  issrngd  15904  divscrng  16266  fitop  16928  tgcl  16989  topbas  16992  ppttop  17026  epttop  17028  restbas  17176  isnrm2  17376  isnrm3  17377  2ndcctbss  17471  txbas  17552  txbasval  17591  txhaus  17632  xkohaus  17638  basqtop  17696  opnfbas  17827  isfild  17843  filfi  17844  neifil  17865  fbasrn  17869  filufint  17905  rnelfmlem  17937  fmfnfmlem3  17941  fmfnfm  17943  blfps  18389  blf  18390  blbas  18413  minveclem3b  19282  aalioulem2  20203  wlkdvspthlem  21560  grpodivf  21787  isabloda  21840  ipf  22165  ocsh  22738  adjadj  23392  unopadj2  23394  hmopadj  23395  hmopbdoptHIL  23444  lnopmi  23456  adjlnop  23542  xreceu  24121  esumcocn  24423  ghomf1olem  25058  dfon2  25362  nocvxmin  25559  axcontlem9  25815  outsideofeu  25969  hilbert1.2  25993  ontopbas  26082  opnrebl2  26214  nn0prpw  26216  fness  26252  tailfb  26296  neificl  26349  metf1o  26351  crngohomfo  26506  smprngopr  26552  ispridlc  26570  prter2  26620  mzpincl  26681  mzpindd  26693  frgrawopreglem4  28150  bnj1384  29107  snatpsubN  30232  pclclN  30373  pclfinN  30382  ltrncnv  30628  cdleme24  30834  cdleme28  30855  cdleme50ltrn  31039  cdleme  31042  ltrnco  31201  cdlemk28-3  31390  diaf11N  31532  dibf11N  31644  dihlsscpre  31717  mapdpg  32189  mapdh9a  32273  mapdh9aOLDN  32274  hdmap14lem6  32359
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 2671
  Copyright terms: Public domain W3C validator