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

Theorem ralbid 3231
 Description: Formula-building rule for restricted universal quantifier (deduction form). (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 483 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 3230 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1780   ∈ wcel 2110  ∀wral 3138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-ral 3143 This theorem is referenced by:  raleqbid  3421  sbcralt  3854  sbcrext  3855  riota5f  7141  zfrep6  7655  cnfcom3clem  9167  cplem2  9318  infxpenc2lem2  9445  acnlem  9473  lble  11592  fsuppmapnn0fiubex  13359  chirred  30171  rspc2daf  30230  aciunf1lem  30406  nosupbnd1  33214  indexa  35007  riotasvd  36091  cdlemk36  38048  choicefi  41461  axccdom  41485  rexabsle  41691  infxrunb3rnmpt  41700  uzublem  41702  climf  41901  climf2  41945  limsupubuzlem  41991  cncficcgt0  42169  stoweidlem16  42300  stoweidlem18  42302  stoweidlem21  42305  stoweidlem29  42313  stoweidlem31  42315  stoweidlem36  42320  stoweidlem41  42325  stoweidlem44  42328  stoweidlem45  42329  stoweidlem51  42335  stoweidlem55  42339  stoweidlem59  42343  stoweidlem60  42344  issmfgelem  43044  smfpimcclem  43080  sprsymrelf  43656
 Copyright terms: Public domain W3C validator