MPE Home 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