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

Theorem ralrimivv 2952
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 450 . . 3 (𝜑 → (𝑥𝐴 → (𝑦𝐵𝜓)))
32ralrimdv 2950 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2947 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ral 2900
This theorem is referenced by:  ralrimivva  2953  ralrimdvv  2955  reuind  3377  disjxiun  4573  disjxiunOLD  4574  somo  4983  ssrel2  5122  sorpsscmpl  6824  f1o2ndf1  7150  soxp  7155  smoiso  7324  smo11  7326  fiint  8100  sornom  8960  axdc4lem  9138  zorn2lem6  9184  fpwwe2lem12  9320  fpwwe2lem13  9321  nqereu  9608  genpnnp  9684  receu  10524  lbreu  10825  injresinj  12409  sqrmo  13789  iscatd  16106  isfuncd  16297  symgextf1  17613  lsmsubm  17840  iscmnd  17977  qusabl  18040  dprdsubg  18195  issrngd  18633  quscrng  19010  mamudm  19961  mat1dimcrng  20050  mavmuldm  20123  fitop  20478  tgcl  20532  topbas  20535  ppttop  20569  epttop  20571  restbas  20720  isnrm2  20920  isnrm3  20921  2ndcctbss  21016  txbas  21128  txbasval  21167  txhaus  21208  xkohaus  21214  basqtop  21272  opnfbas  21404  isfild  21420  filfi  21421  neifil  21442  fbasrn  21446  filufint  21482  rnelfmlem  21514  fmfnfmlem3  21518  fmfnfm  21520  blfps  21969  blf  21970  blbas  21993  minveclem3b  22952  aalioulem2  23837  axcontlem9  25598  wlkdvspthlem  25931  frgrawopreglem4  26368  grpodivf  26570  ipf  26784  ocsh  27360  adjadj  28013  unopadj2  28015  hmopadj  28016  hmopbdoptHIL  28065  lnopmi  28077  adjlnop  28163  xreceu  28795  esumcocn  29303  bnj1384  30188  mclsax  30554  dfon2  30775  nocvxmin  30924  outsideofeu  31242  hilbert1.2  31266  opnrebl2  31320  nn0prpw  31322  fness  31348  tailfb  31376  ontopbas  31431  neificl  32543  metf1o  32545  crngohomfo  32799  smprngopr  32845  ispridlc  32863  prter2  33008  snatpsubN  33878  pclclN  34019  pclfinN  34028  ltrncnv  34274  cdleme24  34482  cdleme28  34503  cdleme50ltrn  34687  cdleme  34690  ltrnco  34849  cdlemk28-3  35038  diaf11N  35180  dibf11N  35292  dihlsscpre  35365  mapdpg  35837  mapdh9a  35921  mapdh9aOLDN  35922  hdmap14lem6  36007  mzpincl  36139  mzpindd  36151  iunconlem2  38017  islptre  38510  upgrwlkdvdelem  40964  frgrwopreglem4  41506  lmod1  42097
  Copyright terms: Public domain W3C validator