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

Theorem ralbida 2979
 Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
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 ((𝜑𝑥𝐴) → (𝜓𝜒))
32pm5.74da 722 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
41, 3albid 2088 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 2914 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 2914 . 2 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63bitr4g 303 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1479  Ⅎwnf 1706   ∈ wcel 1988  ∀wral 2909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708  df-ral 2914 This theorem is referenced by:  ralbid  2980  2ralbida  2984  ralbi  3064  ac6num  9286  neiptopreu  20918  istrkg2ld  25340  funcnv5mpt  29443  xrralrecnnge  39426  climf2  39698  clim2f2  39702  limsupub  39736  climinfmpt  39747  limsupubuzmpt  39751  limsupre2mpt  39762  limsupre3mpt  39766  limsupreuzmpt  39771  smfsupmpt  40784  smfinfmpt  40788
 Copyright terms: Public domain W3C validator