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 228 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralimdaa 3258 . 2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
52biimprd 247 . . 3 ((𝜑𝑥𝐴) → (𝜒𝜓))
61, 5ralimdaa 3258 . 2 (𝜑 → (∀𝑥𝐴 𝜒 → ∀𝑥𝐴 𝜓))
74, 6impbid 211 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wnf 1786  wcel 2107  wral 3062
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 3063
This theorem is referenced by:  ralbid  3271  2ralbida  3281  ac6num  10474  neiptopreu  22637  istrkg2ld  27711  funcnv5mpt  31893  nadd1suc  42142  naddsuc2  42143  xrralrecnnge  44100  climf2  44382  clim2f2  44386  limsupub  44420  climinfmpt  44431  limsupubuzmpt  44435  limsupre2mpt  44446  limsupre3mpt  44450  limsupreuzmpt  44455  xlimmnfmpt  44559  xlimpnfmpt  44560  smfsupmpt  45531  smfinfmpt  45535
  Copyright terms: Public domain W3C validator