Theorem ralbid 3161

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

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1786   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-ral 3069

This theorem is referenced by:  raleqbid  3352  sbcralt  3805  sbcrext  3806  riota5f  7261  zfrep6  7797  cnfcom3clem  9463  cplem2  9648  infxpenc2lem2  9776  acnlem  9804  lble  11927  fsuppmapnn0fiubex  13712  chirred  30757  rspc2daf  30816  aciunf1lem  30999  nosupbnd1  33917  noinfbnd1  33932  indexa  35891  riotasvd  36970  cdlemk36  38927  choicefi  42740  axccdom  42762  rexabsle  42959  infxrunb3rnmpt  42968  uzublem  42970  climf  43163  climf2  43207  limsupubuzlem  43253  cncficcgt0  43429  stoweidlem16  43557  stoweidlem18  43559  stoweidlem21  43562  stoweidlem29  43570  stoweidlem31  43572  stoweidlem36  43577  stoweidlem41  43582  stoweidlem44  43585  stoweidlem45  43586  stoweidlem51  43592  stoweidlem55  43596  stoweidlem59  43600  stoweidlem60  43601  issmfgelem  44304  smfpimcclem  44340  sprsymrelf  44947