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

Theorem ralbida 3131
 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 805 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
41, 3albid 2246 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3066 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3066 . 2 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63bitr4g 303 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382  ∀wal 1629  Ⅎwnf 1856   ∈ wcel 2145  ∀wral 3061 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858  df-ral 3066 This theorem is referenced by:  ralbid  3132  2ralbida  3136  ralbi  3216  ac6num  9503  neiptopreu  21158  istrkg2ld  25580  funcnv5mpt  29809  xrralrecnnge  40129  climf2  40416  clim2f2  40420  limsupub  40454  climinfmpt  40465  limsupubuzmpt  40469  limsupre2mpt  40480  limsupre3mpt  40484  limsupreuzmpt  40489  xlimmnfmpt  40587  xlimpnfmpt  40588  smfsupmpt  41541  smfinfmpt  41545
 Copyright terms: Public domain W3C validator