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  7343  zfrep6OLD  7899  cnfcom3clem  9615  cplem2  9803  infxpenc2lem2  9931  acnlem  9959  lble  12095  fsuppmapnn0fiubex  13916  nosupbnd1  27666  noinfbnd1  27681  chirred  32455  rspc2daf  32524  aciunf1lem  32724  indexa  38045  riotasvd  39393  cdlemk36  41350  modelaxreplem3  45410  choicefi  45632  axccdom  45654  rexabsle  45851  infxrunb3rnmpt  45860  uzublem  45862  climf  46056  climf2  46098  limsupubuzlem  46144  cncficcgt0  46320  stoweidlem16  46448  stoweidlem18  46450  stoweidlem21  46453  stoweidlem29  46461  stoweidlem31  46463  stoweidlem36  46468  stoweidlem41  46473  stoweidlem44  46476  stoweidlem45  46477  stoweidlem51  46483  stoweidlem55  46487  stoweidlem59  46491  stoweidlem60  46492  issmfgelem  47201  smfpimcclem  47239  sprsymrelf  47929