Theorem ralbid 3250

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3160. (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 3248	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  3329  sbcralt  3823  sbcrext  3824  riota5f  7345  zfrep6  7901  cnfcom3clem  9618  cplem2  9806  infxpenc2lem2  9934  acnlem  9962  lble  12098  fsuppmapnn0fiubex  13919  nosupbnd1  27686  noinfbnd1  27701  chirred  32453  rspc2daf  32522  aciunf1lem  32722  indexa  37905  riotasvd  39253  cdlemk36  41210  modelaxreplem3  45257  choicefi  45480  axccdom  45502  rexabsle  45699  infxrunb3rnmpt  45708  uzublem  45710  climf  45904  climf2  45946  limsupubuzlem  45992  cncficcgt0  46168  stoweidlem16  46296  stoweidlem18  46298  stoweidlem21  46301  stoweidlem29  46309  stoweidlem31  46311  stoweidlem36  46316  stoweidlem41  46321  stoweidlem44  46324  stoweidlem45  46325  stoweidlem51  46331  stoweidlem55  46335  stoweidlem59  46339  stoweidlem60  46340  issmfgelem  47049  smfpimcclem  47087  sprsymrelf  47777