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

Theorem ralbida 3249
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 3239 . 2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
52biimprd 247 . . 3 ((𝜑𝑥𝐴) → (𝜒𝜓))
61, 5ralimdaa 3239 . 2 (𝜑 → (∀𝑥𝐴 𝜒 → ∀𝑥𝐴 𝜓))
74, 6impbid 211 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wnf 1784  wcel 2105  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-12 2170
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-nf 1785  df-ral 3062
This theorem is referenced by:  ralbid  3252  2ralbida  3262  ac6num  10336  neiptopreu  22390  istrkg2ld  27110  funcnv5mpt  31292  xrralrecnnge  43265  climf2  43543  clim2f2  43547  limsupub  43581  climinfmpt  43592  limsupubuzmpt  43596  limsupre2mpt  43607  limsupre3mpt  43611  limsupreuzmpt  43616  xlimmnfmpt  43720  xlimpnfmpt  43721  smfsupmpt  44690  smfinfmpt  44694
  Copyright terms: Public domain W3C validator