Theorem ralbid 3251

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3157. (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 1783   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3046

This theorem is referenced by:  raleqbid  3334  sbcralt  3838  sbcrext  3839  riota5f  7375  zfrep6  7936  cnfcom3clem  9665  cplem2  9850  infxpenc2lem2  9980  acnlem  10008  lble  12142  fsuppmapnn0fiubex  13964  nosupbnd1  27633  noinfbnd1  27648  chirred  32331  rspc2daf  32402  aciunf1lem  32593  indexa  37734  riotasvd  38956  cdlemk36  40914  modelaxreplem3  44977  choicefi  45201  axccdom  45223  rexabsle  45422  infxrunb3rnmpt  45431  uzublem  45433  climf  45627  climf2  45671  limsupubuzlem  45717  cncficcgt0  45893  stoweidlem16  46021  stoweidlem18  46023  stoweidlem21  46026  stoweidlem29  46034  stoweidlem31  46036  stoweidlem36  46041  stoweidlem41  46046  stoweidlem44  46049  stoweidlem45  46050  stoweidlem51  46056  stoweidlem55  46060  stoweidlem59  46064  stoweidlem60  46065  issmfgelem  46774  smfpimcclem  46812  sprsymrelf  47500