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

Theorem ralbida 3268
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
Hypotheses
Ref Expression
ralbida.1 𝑥𝜑
ralbida.2 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralbida (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))

Proof of Theorem ralbida
StepHypRef Expression
1 ralbida.1 . . 3 𝑥𝜑
2 ralbida.2 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
32biimpd 229 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralimdaa 3258 . 2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
52biimprd 248 . . 3 ((𝜑𝑥𝐴) → (𝜒𝜓))
61, 5ralimdaa 3258 . 2 (𝜑 → (∀𝑥𝐴 𝜒 → ∀𝑥𝐴 𝜓))
74, 6impbid 212 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wnf 1780  wcel 2106  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-ral 3060
This theorem is referenced by:  ralbid  3271  2ralbida  3281  naddsuc2  8738  ac6num  10517  neiptopreu  23157  istrkg2ld  28483  funcnv5mpt  32685  nadd1suc  43382  xrralrecnnge  45340  climf2  45622  clim2f2  45626  limsupub  45660  climinfmpt  45671  limsupubuzmpt  45675  limsupre2mpt  45686  limsupre3mpt  45690  limsupreuzmpt  45695  xlimmnfmpt  45799  xlimpnfmpt  45800  smfsupmpt  46771  smfinfmpt  46775
  Copyright terms: Public domain W3C validator