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

Theorem ralrimivv 2999
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 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
Assertion
Ref Expression
ralrimivv (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivv
StepHypRef Expression
1 ralrimivv.1 . . . 4 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
21expd 451 . . 3 (𝜑 → (𝑥𝐴 → (𝑦𝐵𝜓)))
32ralrimdv 2997 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2994 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946
This theorem is referenced by:  ralrimivva  3000  ralrimdvv  3002  reuind  3444  disjiund  4675  disjxiun  4681  disjxiunOLD  4682  somo  5098  ssrel2  5244  sorpsscmpl  6990  f1o2ndf1  7330  soxp  7335  smoiso  7504  smo11  7506  fiint  8278  sornom  9137  axdc4lem  9315  zorn2lem6  9361  fpwwe2lem12  9501  fpwwe2lem13  9502  nqereu  9789  genpnnp  9865  receu  10710  lbreu  11011  injresinj  12629  sqrmo  14036  iscatd  16381  isfuncd  16572  symgextf1  17887  lsmsubm  18114  iscmnd  18251  qusabl  18314  dprdsubg  18469  issrngd  18909  quscrng  19288  mamudm  20242  mat1dimcrng  20331  mavmuldm  20404  fitop  20753  tgcl  20821  topbas  20824  ppttop  20859  epttop  20861  restbas  21010  isnrm2  21210  isnrm3  21211  2ndcctbss  21306  txbas  21418  txbasval  21457  txhaus  21498  xkohaus  21504  basqtop  21562  opnfbas  21693  isfild  21709  filfi  21710  neifil  21731  fbasrn  21735  filufint  21771  rnelfmlem  21803  fmfnfmlem3  21807  fmfnfm  21809  blfps  22258  blf  22259  blbas  22282  minveclem3b  23245  aalioulem2  24133  axcontlem9  25897  upgrwlkdvdelem  26688  grpodivf  27520  ipf  27696  ocsh  28270  adjadj  28923  unopadj2  28925  hmopadj  28926  hmopbdoptHIL  28975  lnopmi  28987  adjlnop  29073  xreceu  29758  esumcocn  30270  bnj1384  31226  mclsax  31592  dfon2  31821  nocvxmin  32019  outsideofeu  32363  hilbert1.2  32387  opnrebl2  32441  nn0prpw  32443  fness  32469  tailfb  32497  ontopbas  32552  neificl  33679  metf1o  33681  crngohomfo  33935  smprngopr  33981  ispridlc  33999  prter2  34485  snatpsubN  35354  pclclN  35495  pclfinN  35504  ltrncnv  35750  cdleme24  35957  cdleme28  35978  cdleme50ltrn  36162  cdleme  36165  ltrnco  36324  cdlemk28-3  36513  diaf11N  36655  dibf11N  36767  dihlsscpre  36840  mapdpg  37312  mapdh9a  37396  mapdh9aOLDN  37397  hdmap14lem6  37482  mzpincl  37614  mzpindd  37626  iunconnlem2  39485  islptre  40169  lmod1  42606
  Copyright terms: Public domain W3C validator