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

Theorem ralbid 3255
Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3171. (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 482 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 3252 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wnf 1786  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3062
This theorem is referenced by:  raleqbid  3329  sbcralt  3829  sbcrext  3830  riota5f  7343  zfrep6  7888  cnfcom3clem  9646  cplem2  9831  infxpenc2lem2  9961  acnlem  9989  lble  12112  fsuppmapnn0fiubex  13903  nosupbnd1  27078  noinfbnd1  27093  chirred  31379  rspc2daf  31439  aciunf1lem  31624  indexa  36238  riotasvd  37464  cdlemk36  39422  choicefi  43508  axccdom  43530  rexabsle  43740  infxrunb3rnmpt  43749  uzublem  43751  climf  43949  climf2  43993  limsupubuzlem  44039  cncficcgt0  44215  stoweidlem16  44343  stoweidlem18  44345  stoweidlem21  44348  stoweidlem29  44356  stoweidlem31  44358  stoweidlem36  44363  stoweidlem41  44368  stoweidlem44  44371  stoweidlem45  44372  stoweidlem51  44378  stoweidlem55  44382  stoweidlem59  44386  stoweidlem60  44387  issmfgelem  45096  smfpimcclem  45134  sprsymrelf  45773
  Copyright terms: Public domain W3C validator