Theorem ralbid 3248

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3156. (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 3246	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  raleqbid  3329  sbcralt  3832  sbcrext  3833  riota5f  7354  zfrep6  7913  cnfcom3clem  9634  cplem2  9819  infxpenc2lem2  9949  acnlem  9977  lble  12111  fsuppmapnn0fiubex  13933  nosupbnd1  27659  noinfbnd1  27674  chirred  32374  rspc2daf  32445  aciunf1lem  32636  indexa  37720  riotasvd  38942  cdlemk36  40900  modelaxreplem3  44963  choicefi  45187  axccdom  45209  rexabsle  45408  infxrunb3rnmpt  45417  uzublem  45419  climf  45613  climf2  45657  limsupubuzlem  45703  cncficcgt0  45879  stoweidlem16  46007  stoweidlem18  46009  stoweidlem21  46012  stoweidlem29  46020  stoweidlem31  46022  stoweidlem36  46027  stoweidlem41  46032  stoweidlem44  46035  stoweidlem45  46036  stoweidlem51  46042  stoweidlem55  46046  stoweidlem59  46050  stoweidlem60  46051  issmfgelem  46760  smfpimcclem  46798  sprsymrelf  47489