Theorem ralbid 3253

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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 3251	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3055

This theorem is referenced by:  raleqbid  3323  sbcralt  3811  sbcrext  3812  riota5f  7348  zfrep6OLD  7904  cnfcom3clem  9624  cplem2  9812  infxpenc2lem2  9940  acnlem  9968  lble  12106  fsuppmapnn0fiubex  13952  nosupbnd1  27703  noinfbnd1  27718  chirred  32491  rspc2daf  32560  aciunf1lem  32761  indexa  38101  riotasvd  39449  cdlemk36  41406  modelaxreplem3  45425  choicefi  45647  axccdom  45668  rexabsle  45863  infxrunb3rnmpt  45872  uzublem  45874  climf  46068  climf2  46110  limsupubuzlem  46156  cncficcgt0  46332  stoweidlem16  46460  stoweidlem18  46462  stoweidlem21  46465  stoweidlem29  46473  stoweidlem31  46475  stoweidlem36  46480  stoweidlem41  46485  stoweidlem44  46488  stoweidlem45  46489  stoweidlem51  46495  stoweidlem55  46499  stoweidlem59  46503  stoweidlem60  46504  issmfgelem  47213  smfpimcclem  47251  sprsymrelf  47971