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

Theorem ralbid 3130
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 472 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
41, 3ralbida 3129 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wnf 1878  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-nf 1879  df-ral 3060
This theorem is referenced by:  raleqbid  3298  sbcralt  3671  sbcrext  3672  riota5f  6830  zfrep6  7334  cnfcom3clem  8819  cplem2  8970  infxpenc2lem2  9096  acnlem  9124  lble  11231  fsuppmapnn0fiubex  13002  chirred  29713  aciunf1lem  29915  nosupbnd1  32307  indexa  33954  riotasvd  34915  cdlemk36  36872  choicefi  40040  axccdom  40064  rexabsle  40286  infxrunb3rnmpt  40295  uzublem  40297  climf  40495  climf2  40539  limsupubuzlem  40585  cncficcgt0  40742  stoweidlem16  40873  stoweidlem18  40875  stoweidlem21  40878  stoweidlem29  40886  stoweidlem31  40888  stoweidlem36  40893  stoweidlem41  40898  stoweidlem44  40901  stoweidlem45  40902  stoweidlem51  40908  stoweidlem55  40912  stoweidlem59  40916  stoweidlem60  40917  issmfgelem  41620  smfpimcclem  41656  sprsymrelf  42417
  Copyright terms: Public domain W3C validator