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

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

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