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

Theorem ralbid 2979
 Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)
Hypotheses
Ref Expression
ralbid.1 𝑥𝜑
ralbid.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralbid (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))

Proof of Theorem ralbid
StepHypRef Expression
1 ralbid.1 . 2 𝑥𝜑
2 ralbid.2 . . 3 (𝜑 → (𝜓𝜒))
32adantr 481 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 2978 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1705   ∈ wcel 1987  ∀wral 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-nf 1707  df-ral 2913 This theorem is referenced by:  raleqbid  3143  sbcralt  3497  sbcrext  3498  sbcrextOLD  3499  riota5f  6601  zfrep6  7096  cnfcom3clem  8562  cplem2  8713  infxpenc2lem2  8803  acnlem  8831  lble  10935  fsuppmapnn0fiubex  12748  chirred  29142  aciunf1lem  29345  indexa  33199  riotasvd  33761  cdlemk36  35720  choicefi  38901  axccdom  38925  rexabsle  39145  infxrunb3rnmpt  39154  uzublem  39156  climf  39290  climf2  39334  limsupubuzlem  39380  cncficcgt0  39436  stoweidlem16  39570  stoweidlem18  39572  stoweidlem21  39575  stoweidlem29  39583  stoweidlem31  39585  stoweidlem36  39590  stoweidlem41  39595  stoweidlem44  39598  stoweidlem45  39599  stoweidlem51  39605  stoweidlem55  39609  stoweidlem59  39613  stoweidlem60  39614  issmfgelem  40314  smfpimcclem  40350  sprsymrelf  41063
 Copyright terms: Public domain W3C validator