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  3321  sbcralt  3811  sbcrext  3812  riota5f  7352  zfrep6OLD  7908  cnfcom3clem  9626  cplem2  9814  infxpenc2lem2  9942  acnlem  9970  lble  12108  fsuppmapnn0fiubex  13954  nosupbnd1  27678  noinfbnd1  27693  chirred  32466  rspc2daf  32535  aciunf1lem  32735  indexa  38054  riotasvd  39402  cdlemk36  41359  modelaxreplem3  45407  choicefi  45629  axccdom  45651  rexabsle  45847  infxrunb3rnmpt  45856  uzublem  45858  climf  46052  climf2  46094  limsupubuzlem  46140  cncficcgt0  46316  stoweidlem16  46444  stoweidlem18  46446  stoweidlem21  46449  stoweidlem29  46457  stoweidlem31  46459  stoweidlem36  46464  stoweidlem41  46469  stoweidlem44  46472  stoweidlem45  46473  stoweidlem51  46479  stoweidlem55  46483  stoweidlem59  46487  stoweidlem60  46488  issmfgelem  47197  smfpimcclem  47235  sprsymrelf  47949