Theorem ralbid 3271

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 482	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3268	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  raleqbid  3353  sbcralt  3867  sbcrext  3868  riota5f  7394  zfrep6  7941  cnfcom3clem  9700  cplem2  9885  infxpenc2lem2  10015  acnlem  10043  lble  12166  fsuppmapnn0fiubex  13957  nosupbnd1  27217  noinfbnd1  27232  chirred  31648  rspc2daf  31708  aciunf1lem  31887  indexa  36601  riotasvd  37826  cdlemk36  39784  choicefi  43899  axccdom  43921  rexabsle  44129  infxrunb3rnmpt  44138  uzublem  44140  climf  44338  climf2  44382  limsupubuzlem  44428  cncficcgt0  44604  stoweidlem16  44732  stoweidlem18  44734  stoweidlem21  44737  stoweidlem29  44745  stoweidlem31  44747  stoweidlem36  44752  stoweidlem41  44757  stoweidlem44  44760  stoweidlem45  44761  stoweidlem51  44767  stoweidlem55  44771  stoweidlem59  44775  stoweidlem60  44776  issmfgelem  45485  smfpimcclem  45523  sprsymrelf  46163