Theorem ralbid 3231

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-ral 3143

This theorem is referenced by:  raleqbid  3421  sbcralt  3855  sbcrext  3856  riota5f  7142  zfrep6  7656  cnfcom3clem  9168  cplem2  9319  infxpenc2lem2  9446  acnlem  9474  lble  11593  fsuppmapnn0fiubex  13361  chirred  30172  rspc2daf  30231  aciunf1lem  30407  nosupbnd1  33214  indexa  35023  riotasvd  36107  cdlemk36  38064  choicefi  41512  axccdom  41536  rexabsle  41742  infxrunb3rnmpt  41751  uzublem  41753  climf  41952  climf2  41996  limsupubuzlem  42042  cncficcgt0  42220  stoweidlem16  42350  stoweidlem18  42352  stoweidlem21  42355  stoweidlem29  42363  stoweidlem31  42365  stoweidlem36  42370  stoweidlem41  42375  stoweidlem44  42378  stoweidlem45  42379  stoweidlem51  42385  stoweidlem55  42389  stoweidlem59  42393  stoweidlem60  42394  issmfgelem  43094  smfpimcclem  43130  sprsymrelf  43706