Theorem ralbid 3251

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3161. (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 3249	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  raleqbid  3330  sbcralt  3824  sbcrext  3825  riota5f  7353  zfrep6  7909  cnfcom3clem  9626  cplem2  9814  infxpenc2lem2  9942  acnlem  9970  lble  12106  fsuppmapnn0fiubex  13927  nosupbnd1  27694  noinfbnd1  27709  chirred  32482  rspc2daf  32551  aciunf1lem  32751  indexa  37973  riotasvd  39321  cdlemk36  41278  modelaxreplem3  45325  choicefi  45547  axccdom  45569  rexabsle  45766  infxrunb3rnmpt  45775  uzublem  45777  climf  45971  climf2  46013  limsupubuzlem  46059  cncficcgt0  46235  stoweidlem16  46363  stoweidlem18  46365  stoweidlem21  46368  stoweidlem29  46376  stoweidlem31  46378  stoweidlem36  46383  stoweidlem41  46388  stoweidlem44  46391  stoweidlem45  46392  stoweidlem51  46398  stoweidlem55  46402  stoweidlem59  46406  stoweidlem60  46407  issmfgelem  47116  smfpimcclem  47154  sprsymrelf  47844