Theorem ralbid 3278

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3188. (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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3276	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1806   ∈ wcel 2145  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-ral 3080

This theorem is referenced by:  raleqbid  3348  sbcralt  3828  sbcrext  3829  riota5f  7385  zfrep6OLD  7940  cnfcom3clem  9662  cplem2  9864  infxpenc2lem2  9992  acnlem  10020  lble  12158  fsuppmapnn0fiubex  14019  nosupbnd1  27836  noinfbnd1  27851  chirred  32656  rspc2daf  32723  aciunf1lem  32919  indexa  38244  riotasvd  39592  cdlemk36  41549  modelaxreplem3  45554  choicefi  45775  axccdom  45796  rexabsle  45991  infxrunb3rnmpt  46000  uzublem  46002  climf  46196  climf2  46238  limsupubuzlem  46284  cncficcgt0  46460  stoweidlem16  46588  stoweidlem18  46590  stoweidlem21  46593  stoweidlem29  46601  stoweidlem31  46603  stoweidlem36  46608  stoweidlem41  46613  stoweidlem44  46616  stoweidlem45  46617  stoweidlem51  46623  stoweidlem55  46627  stoweidlem59  46631  stoweidlem60  46632  issmfgelem  47341  smfpimcclem  47379  sprsymrelf  48099