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

Theorem ralrimivv 2953
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 2951 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2948 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901
This theorem is referenced by:  ralrimivva  2954  ralrimdvv  2956  reuind  3378  disjxiun  4579  disjxiunOLD  4580  somo  4993  ssrel2  5133  sorpsscmpl  6846  f1o2ndf1  7172  soxp  7177  smoiso  7346  smo11  7348  fiint  8122  sornom  8982  axdc4lem  9160  zorn2lem6  9206  fpwwe2lem12  9342  fpwwe2lem13  9343  nqereu  9630  genpnnp  9706  receu  10551  lbreu  10852  injresinj  12451  sqrmo  13840  iscatd  16157  isfuncd  16348  symgextf1  17664  lsmsubm  17891  iscmnd  18028  qusabl  18091  dprdsubg  18246  issrngd  18684  quscrng  19061  mamudm  20013  mat1dimcrng  20102  mavmuldm  20175  fitop  20530  tgcl  20584  topbas  20587  ppttop  20621  epttop  20623  restbas  20772  isnrm2  20972  isnrm3  20973  2ndcctbss  21068  txbas  21180  txbasval  21219  txhaus  21260  xkohaus  21266  basqtop  21324  opnfbas  21456  isfild  21472  filfi  21473  neifil  21494  fbasrn  21498  filufint  21534  rnelfmlem  21566  fmfnfmlem3  21570  fmfnfm  21572  blfps  22021  blf  22022  blbas  22045  minveclem3b  23007  aalioulem2  23892  axcontlem9  25652  wlkdvspthlem  26137  frgrawopreglem4  26574  grpodivf  26776  ipf  26952  ocsh  27526  adjadj  28179  unopadj2  28181  hmopadj  28182  hmopbdoptHIL  28231  lnopmi  28243  adjlnop  28329  xreceu  28961  esumcocn  29469  bnj1384  30354  mclsax  30720  dfon2  30941  nocvxmin  31090  outsideofeu  31408  hilbert1.2  31432  opnrebl2  31486  nn0prpw  31488  fness  31514  tailfb  31542  ontopbas  31597  neificl  32719  metf1o  32721  crngohomfo  32975  smprngopr  33021  ispridlc  33039  prter2  33184  snatpsubN  34054  pclclN  34195  pclfinN  34204  ltrncnv  34450  cdleme24  34658  cdleme28  34679  cdleme50ltrn  34863  cdleme  34866  ltrnco  35025  cdlemk28-3  35214  diaf11N  35356  dibf11N  35468  dihlsscpre  35541  mapdpg  36013  mapdh9a  36097  mapdh9aOLDN  36098  hdmap14lem6  36183  mzpincl  36315  mzpindd  36327  iunconlem2  38193  islptre  38686  upgrwlkdvdelem  40942  frgrwopreglem4  41484  lmod1  42075
  Copyright terms: Public domain W3C validator