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

Theorem ralrimivv 3180
 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 419 . . 3 (𝜑 → (𝑥𝐴 → (𝑦𝐵𝜓)))
32ralrimdv 3178 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 3173 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  ∀wral 3130 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3135 This theorem is referenced by:  ralrimivva  3181  ralrimdvv  3183  reuind  3719  disjiund  5032  disjxiun  5039  somo  5487  ssrel2  5636  sorpsscmpl  7445  f1o2ndf1  7805  soxp  7810  smoiso  7986  smo11  7988  fiint  8783  sornom  9688  axdc4lem  9866  zorn2lem6  9912  fpwwe2lem12  10052  fpwwe2lem13  10053  nqereu  10340  genpnnp  10416  receu  11274  lbreu  11578  injresinj  13153  sqrmo  14602  iscatd  16935  isfuncd  17126  0subm  17973  insubm  17974  sursubmefmnd  18052  injsubmefmnd  18053  cycsubm  18336  symgextf1  18540  lsmsubm  18769  iscmnd  18910  qusabl  18976  cycsubmcmn  18999  dprdsubg  19137  issrngd  19623  quscrng  20004  mamudm  20993  mat1dimcrng  21080  mavmuldm  21153  fitop  21503  tgcl  21572  topbas  21575  ppttop  21610  epttop  21612  restbas  21761  isnrm2  21961  isnrm3  21962  2ndcctbss  22058  txbas  22170  txbasval  22209  txhaus  22250  xkohaus  22256  basqtop  22314  opnfbas  22445  isfild  22461  filfi  22462  neifil  22483  fbasrn  22487  filufint  22523  rnelfmlem  22555  fmfnfmlem3  22559  fmfnfm  22561  blfps  23011  blf  23012  blbas  23035  minveclem3b  24030  aalioulem2  24927  axcontlem9  26764  upgrwlkdvdelem  27523  grpodivf  28319  ipf  28494  ocsh  29064  adjadj  29717  unopadj2  29719  hmopadj  29720  hmopbdoptHIL  29769  lnopmi  29781  adjlnop  29867  xreceu  30608  esumcocn  31413  bnj1384  32378  f1resrcmplf1d  32434  mclsax  32890  dfon2  33111  nocvxmin  33322  outsideofeu  33666  hilbert1.2  33690  opnrebl2  33743  nn0prpw  33745  fness  33771  tailfb  33799  ontopbas  33850  neificl  35149  metf1o  35151  crngohomfo  35402  smprngopr  35448  ispridlc  35466  prter2  36135  snatpsubN  37004  pclclN  37145  pclfinN  37154  ltrncnv  37400  cdleme24  37606  cdleme28  37627  cdleme50ltrn  37811  cdleme  37814  ltrnco  37973  cdlemk28-3  38162  diaf11N  38303  dibf11N  38415  dihlsscpre  38488  mapdpg  38960  mapdh9a  39043  mapdh9aOLDN  39044  hdmap14lem6  39127  mzpincl  39605  mzpindd  39617  iunconnlem2  41575  islptre  42200  2reu8i  43608  lmod1  44840
 Copyright terms: Public domain W3C validator