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

Theorem ralbid 3273
Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3178. (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 3270 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wnf 1783  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3062
This theorem is referenced by:  raleqbid  3356  sbcralt  3872  sbcrext  3873  riota5f  7416  zfrep6  7979  cnfcom3clem  9745  cplem2  9930  infxpenc2lem2  10060  acnlem  10088  lble  12220  fsuppmapnn0fiubex  14033  nosupbnd1  27759  noinfbnd1  27774  chirred  32414  rspc2daf  32485  aciunf1lem  32672  indexa  37740  riotasvd  38957  cdlemk36  40915  modelaxreplem3  44997  choicefi  45205  axccdom  45227  rexabsle  45430  infxrunb3rnmpt  45439  uzublem  45441  climf  45637  climf2  45681  limsupubuzlem  45727  cncficcgt0  45903  stoweidlem16  46031  stoweidlem18  46033  stoweidlem21  46036  stoweidlem29  46044  stoweidlem31  46046  stoweidlem36  46051  stoweidlem41  46056  stoweidlem44  46059  stoweidlem45  46060  stoweidlem51  46066  stoweidlem55  46070  stoweidlem59  46074  stoweidlem60  46075  issmfgelem  46784  smfpimcclem  46822  sprsymrelf  47482
  Copyright terms: Public domain W3C validator