Theorem ralbid 3195

Description: Formula-building rule for restricted universal quantifier (deduction form). (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 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3194	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3111

This theorem is referenced by:  raleqbid  3368  sbcralt  3801  sbcrext  3802  riota5f  7121  zfrep6  7638  cnfcom3clem  9152  cplem2  9303  infxpenc2lem2  9431  acnlem  9459  lble  11580  fsuppmapnn0fiubex  13355  chirred  30178  rspc2daf  30238  aciunf1lem  30425  nosupbnd1  33327  indexa  35171  riotasvd  36252  cdlemk36  38209  choicefi  41829  axccdom  41853  rexabsle  42056  infxrunb3rnmpt  42065  uzublem  42067  climf  42264  climf2  42308  limsupubuzlem  42354  cncficcgt0  42530  stoweidlem16  42658  stoweidlem18  42660  stoweidlem21  42663  stoweidlem29  42671  stoweidlem31  42673  stoweidlem36  42678  stoweidlem41  42683  stoweidlem44  42686  stoweidlem45  42687  stoweidlem51  42693  stoweidlem55  42697  stoweidlem59  42701  stoweidlem60  42702  issmfgelem  43402  smfpimcclem  43438  sprsymrelf  44012