Theorem ralbid 3276

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3186. (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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3274	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1811   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-12 2211

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-nf 1812  df-ral 3078

This theorem is referenced by:  raleqbid  3345  sbcralt  3824  sbcrext  3825  riota5f  7395  zfrep6OLD  7951  cnfcom3clem  9673  cplem2  9875  infxpenc2lem2  10003  acnlem  10031  lble  12166  fsuppmapnn0fiubex  14028  nosupbnd1  27854  noinfbnd1  27869  chirred  32713  rspc2daf  32779  aciunf1lem  32973  indexa  38350  riotasvd  39698  cdlemk36  41655  modelaxreplem3  45659  choicefi  45887  axccdom  45908  rexabsle  46103  infxrunb3rnmpt  46112  uzublem  46114  climf  46308  climf2  46350  limsupubuzlem  46396  cncficcgt0  46572  stoweidlem16  46700  stoweidlem18  46702  stoweidlem21  46705  stoweidlem29  46713  stoweidlem31  46715  stoweidlem36  46720  stoweidlem41  46725  stoweidlem44  46728  stoweidlem45  46729  stoweidlem51  46735  stoweidlem55  46739  stoweidlem59  46743  stoweidlem60  46744  issmfgelem  47453  smfpimcclem  47491  sprsymrelf  48211