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  12097  fsuppmapnn0fiubex  13943  nosupbnd1  27697  noinfbnd1  27712  chirred  32486  rspc2daf  32555  aciunf1lem  32755  indexa  38065  riotasvd  39413  cdlemk36  41370  modelaxreplem3  45422  choicefi  45644  axccdom  45666  rexabsle  45862  infxrunb3rnmpt  45871  uzublem  45873  climf  46067  climf2  46109  limsupubuzlem  46155  cncficcgt0  46331  stoweidlem16  46459  stoweidlem18  46461  stoweidlem21  46464  stoweidlem29  46472  stoweidlem31  46474  stoweidlem36  46479  stoweidlem41  46484  stoweidlem44  46487  stoweidlem45  46488  stoweidlem51  46494  stoweidlem55  46498  stoweidlem59  46502  stoweidlem60  46503  issmfgelem  47212  smfpimcclem  47250  sprsymrelf  47952