Theorem ralbid 3271

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3176. (Contributed by NM, 27-Jun-1998.)

Hypotheses

Ref	Expression
ralbid.1	⊢ Ⅎ𝑥𝜑
ralbid.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbid	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Proof of Theorem ralbid

Step	Hyp	Ref	Expression
1		ralbid.1	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbid.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3268	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1780   ∈ wcel 2106  ∀wral 3059

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 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-ral 3060

This theorem is referenced by:  raleqbid  3354  sbcralt  3881  sbcrext  3882  riota5f  7416  zfrep6  7978  cnfcom3clem  9743  cplem2  9928  infxpenc2lem2  10058  acnlem  10086  lble  12218  fsuppmapnn0fiubex  14030  nosupbnd1  27774  noinfbnd1  27789  chirred  32424  rspc2daf  32495  aciunf1lem  32679  indexa  37720  riotasvd  38938  cdlemk36  40896  modelaxreplem3  44945  choicefi  45143  axccdom  45165  rexabsle  45369  infxrunb3rnmpt  45378  uzublem  45380  climf  45578  climf2  45622  limsupubuzlem  45668  cncficcgt0  45844  stoweidlem16  45972  stoweidlem18  45974  stoweidlem21  45977  stoweidlem29  45985  stoweidlem31  45987  stoweidlem36  45992  stoweidlem41  45997  stoweidlem44  46000  stoweidlem45  46001  stoweidlem51  46007  stoweidlem55  46011  stoweidlem59  46015  stoweidlem60  46016  issmfgelem  46725  smfpimcclem  46763  sprsymrelf  47420