Theorem ralbid 3242

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3152. (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 3240	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  3321  sbcralt  3824  sbcrext  3825  riota5f  7334  zfrep6  7890  cnfcom3clem  9601  cplem2  9786  infxpenc2lem2  9914  acnlem  9942  lble  12077  fsuppmapnn0fiubex  13899  nosupbnd1  27624  noinfbnd1  27639  chirred  32343  rspc2daf  32414  aciunf1lem  32613  indexa  37733  riotasvd  38955  cdlemk36  40912  modelaxreplem3  44974  choicefi  45198  axccdom  45220  rexabsle  45418  infxrunb3rnmpt  45427  uzublem  45429  climf  45623  climf2  45667  limsupubuzlem  45713  cncficcgt0  45889  stoweidlem16  46017  stoweidlem18  46019  stoweidlem21  46022  stoweidlem29  46030  stoweidlem31  46032  stoweidlem36  46037  stoweidlem41  46042  stoweidlem44  46045  stoweidlem45  46046  stoweidlem51  46052  stoweidlem55  46056  stoweidlem59  46060  stoweidlem60  46061  issmfgelem  46770  smfpimcclem  46808  sprsymrelf  47499