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

Theorem ralbid 2966
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 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 2965 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wnf 1699  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901
This theorem is referenced by:  raleqbid  3127  sbcralt  3477  sbcrext  3478  sbcrextOLD  3479  riota5f  6535  zfrep6  7027  cnfcom3clem  8485  cplem2  8636  infxpenc2lem2  8726  acnlem  8754  lble  10854  fsuppmapnn0fiubex  12654  chirred  28638  aciunf1lem  28844  indexa  32698  riotasvd  33260  cdlemk36  35219  choicefi  38387  axccdom  38411  climf  38689  climf2  38733  cncficcgt0  38774  stoweidlem16  38909  stoweidlem18  38911  stoweidlem21  38914  stoweidlem29  38922  stoweidlem31  38924  stoweidlem36  38929  stoweidlem41  38934  stoweidlem44  38937  stoweidlem45  38938  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  stoweidlem60  38953  issmfgelem  39655
  Copyright terms: Public domain W3C validator