Theorem ralbid 3255

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

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

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 2007  ax-12 2177

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

This theorem is referenced by:  raleqbid  3335  sbcralt  3847  sbcrext  3848  riota5f  7390  zfrep6  7953  cnfcom3clem  9719  cplem2  9904  infxpenc2lem2  10034  acnlem  10062  lble  12194  fsuppmapnn0fiubex  14010  nosupbnd1  27678  noinfbnd1  27693  chirred  32376  rspc2daf  32447  aciunf1lem  32640  indexa  37757  riotasvd  38974  cdlemk36  40932  modelaxreplem3  45005  choicefi  45224  axccdom  45246  rexabsle  45446  infxrunb3rnmpt  45455  uzublem  45457  climf  45651  climf2  45695  limsupubuzlem  45741  cncficcgt0  45917  stoweidlem16  46045  stoweidlem18  46047  stoweidlem21  46050  stoweidlem29  46058  stoweidlem31  46060  stoweidlem36  46065  stoweidlem41  46070  stoweidlem44  46073  stoweidlem45  46074  stoweidlem51  46080  stoweidlem55  46084  stoweidlem59  46088  stoweidlem60  46089  issmfgelem  46798  smfpimcclem  46836  sprsymrelf  47509