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

Theorem ralbida 3252
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 228 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralimdaa 3242 . 2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
52biimprd 248 . . 3 ((𝜑𝑥𝐴) → (𝜒𝜓))
61, 5ralimdaa 3242 . 2 (𝜑 → (∀𝑥𝐴 𝜒 → ∀𝑥𝐴 𝜓))
74, 6impbid 211 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wnf 1786  wcel 2107  wral 3063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3064
This theorem is referenced by:  ralbid  3255  2ralbida  3265  ac6num  10349  neiptopreu  22412  istrkg2ld  27207  funcnv5mpt  31388  xrralrecnnge  43420  climf2  43698  clim2f2  43702  limsupub  43736  climinfmpt  43747  limsupubuzmpt  43751  limsupre2mpt  43762  limsupre3mpt  43766  limsupreuzmpt  43771  xlimmnfmpt  43875  xlimpnfmpt  43876  smfsupmpt  44847  smfinfmpt  44851
  Copyright terms: Public domain W3C validator