Theorem ralbid 3274

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1802   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-ral 3076

This theorem is referenced by:  raleqbid  3344  sbcralt  3825  sbcrext  3826  riota5f  7375  zfrep6OLD  7930  cnfcom3clem  9655  cplem2  9843  infxpenc2lem2  9971  acnlem  9999  lble  12139  fsuppmapnn0fiubex  14000  nosupbnd1  27753  noinfbnd1  27768  chirred  32542  rspc2daf  32611  aciunf1lem  32812  indexa  38185  riotasvd  39533  cdlemk36  41490  modelaxreplem3  45509  choicefi  45730  axccdom  45751  rexabsle  45946  infxrunb3rnmpt  45955  uzublem  45957  climf  46151  climf2  46193  limsupubuzlem  46239  cncficcgt0  46415  stoweidlem16  46543  stoweidlem18  46545  stoweidlem21  46548  stoweidlem29  46556  stoweidlem31  46558  stoweidlem36  46563  stoweidlem41  46568  stoweidlem44  46571  stoweidlem45  46572  stoweidlem51  46578  stoweidlem55  46582  stoweidlem59  46586  stoweidlem60  46587  issmfgelem  47296  smfpimcclem  47334  sprsymrelf  48054