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

Theorem ralbida 3129
Description: Formula-building rule for restricted universal quantifier (deduction form). (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 838 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
41, 3albid 2255 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐴𝜒)))
5 df-ral 3060 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
6 df-ral 3060 . 2 (∀𝑥𝐴 𝜒 ↔ ∀𝑥(𝑥𝐴𝜒))
74, 5, 63bitr4g 305 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1650  wnf 1878  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-nf 1879  df-ral 3060
This theorem is referenced by:  ralbid  3130  2ralbida  3134  ralbi  3215  ac6num  9554  neiptopreu  21217  istrkg2ld  25650  funcnv5mpt  29918  xrralrecnnge  40250  climf2  40536  clim2f2  40540  limsupub  40574  climinfmpt  40585  limsupubuzmpt  40589  limsupre2mpt  40600  limsupre3mpt  40604  limsupreuzmpt  40609  xlimmnfmpt  40707  xlimpnfmpt  40708  smfsupmpt  41661  smfinfmpt  41665
  Copyright terms: Public domain W3C validator