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  9636  cplem2  9821  infxpenc2lem2  9951  acnlem  9979  lble  12113  fsuppmapnn0fiubex  13935  nosupbnd1  27660  noinfbnd1  27675  chirred  32375  rspc2daf  32446  aciunf1lem  32637  indexa  37721  riotasvd  38943  cdlemk36  40901  modelaxreplem3  44964  choicefi  45188  axccdom  45210  rexabsle  45409  infxrunb3rnmpt  45418  uzublem  45420  climf  45614  climf2  45658  limsupubuzlem  45704  cncficcgt0  45880  stoweidlem16  46008  stoweidlem18  46010  stoweidlem21  46013  stoweidlem29  46021  stoweidlem31  46023  stoweidlem36  46028  stoweidlem41  46033  stoweidlem44  46036  stoweidlem45  46037  stoweidlem51  46043  stoweidlem55  46047  stoweidlem59  46051  stoweidlem60  46052  issmfgelem  46761  smfpimcclem  46799  sprsymrelf  47490