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

Theorem ralbid 3113
 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 472 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 3112 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1849   ∈ wcel 2131  ∀wral 3042 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-12 2188 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-nf 1851  df-ral 3047 This theorem is referenced by:  raleqbid  3281  sbcralt  3643  sbcrext  3644  sbcrextOLD  3645  riota5f  6791  zfrep6  7291  cnfcom3clem  8767  cplem2  8918  infxpenc2lem2  9025  acnlem  9053  lble  11159  fsuppmapnn0fiubex  12978  chirred  29555  aciunf1lem  29763  nosupbnd1  32158  indexa  33833  riotasvd  34737  cdlemk36  36695  choicefi  39883  axccdom  39907  rexabsle  40136  infxrunb3rnmpt  40145  uzublem  40147  climf  40349  climf2  40393  limsupubuzlem  40439  cncficcgt0  40596  stoweidlem16  40728  stoweidlem18  40730  stoweidlem21  40733  stoweidlem29  40741  stoweidlem31  40743  stoweidlem36  40748  stoweidlem41  40753  stoweidlem44  40756  stoweidlem45  40757  stoweidlem51  40763  stoweidlem55  40767  stoweidlem59  40771  stoweidlem60  40772  issmfgelem  41475  smfpimcclem  41511  sprsymrelf  42247
 Copyright terms: Public domain W3C validator