Theorem ralbid 3160

Description: Formula-building rule for restricted universal quantifier (deduction form). (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 3158	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1789   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-nf 1790  df-ral 3070

This theorem is referenced by:  raleqbid  3350  sbcralt  3809  sbcrext  3810  riota5f  7254  zfrep6  7784  cnfcom3clem  9424  cplem2  9632  infxpenc2lem2  9760  acnlem  9788  lble  11910  fsuppmapnn0fiubex  13693  chirred  30736  rspc2daf  30795  aciunf1lem  30978  nosupbnd1  33896  noinfbnd1  33911  indexa  35870  riotasvd  36949  cdlemk36  38906  choicefi  42693  axccdom  42715  rexabsle  42913  infxrunb3rnmpt  42922  uzublem  42924  climf  43117  climf2  43161  limsupubuzlem  43207  cncficcgt0  43383  stoweidlem16  43511  stoweidlem18  43513  stoweidlem21  43516  stoweidlem29  43524  stoweidlem31  43526  stoweidlem36  43531  stoweidlem41  43536  stoweidlem44  43539  stoweidlem45  43540  stoweidlem51  43546  stoweidlem55  43550  stoweidlem59  43554  stoweidlem60  43555  issmfgelem  44255  smfpimcclem  44291  sprsymrelf  44899