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

Theorem ralbida 3269
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 3259 . 2 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
52biimprd 248 . . 3 ((𝜑𝑥𝐴) → (𝜒𝜓))
61, 5ralimdaa 3259 . 2 (𝜑 → (∀𝑥𝐴 𝜒 → ∀𝑥𝐴 𝜓))
74, 6impbid 212 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wnf 1782  wcel 2107  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-ral 3061
This theorem is referenced by:  ralbid  3272  2ralbida  3282  naddsuc2  8740  ac6num  10520  neiptopreu  23142  istrkg2ld  28469  funcnv5mpt  32679  nadd1suc  43410  xrralrecnnge  45406  climf2  45686  clim2f2  45690  limsupub  45724  climinfmpt  45735  limsupubuzmpt  45739  limsupre2mpt  45750  limsupre3mpt  45754  limsupreuzmpt  45759  xlimmnfmpt  45863  xlimpnfmpt  45864  smfsupmpt  46835  smfinfmpt  46839
  Copyright terms: Public domain W3C validator