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  31679  rspc2daf  31739  aciunf1lem  31918  indexa  36649  riotasvd  37874  cdlemk36  39832  choicefi  43947  axccdom  43969  rexabsle  44177  infxrunb3rnmpt  44186  uzublem  44188  climf  44386  climf2  44430  limsupubuzlem  44476  cncficcgt0  44652  stoweidlem16  44780  stoweidlem18  44782  stoweidlem21  44785  stoweidlem29  44793  stoweidlem31  44795  stoweidlem36  44800  stoweidlem41  44805  stoweidlem44  44808  stoweidlem45  44809  stoweidlem51  44815  stoweidlem55  44819  stoweidlem59  44823  stoweidlem60  44824  issmfgelem  45533  smfpimcclem  45571  sprsymrelf  46211