Theorem ralbid 3281

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816   ∈ wcel 2146  ∀wral 3082

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3083

This theorem is used by:  raleqbid  3350  sbcralt  3828  sbcrext  3829  riota5f  7408  zfrep6OLD  7961  cnfcom3clem  9684  cplem2  9891  cplem2OLD  9892  infxpenc2lem2  10023  acnlem  10051  lble  12185  fsuppmapnn0fiubex  14048  nosupbnd1  27908  noinfbnd1  27923  chirred  32777  rspc2daf  32843  aciunf1lem  33037  indexa  38417  riotasvd  39763  cdlemk36  41720  modelaxreplem3  45722  choicefi  45950  axccdom  45971  rexabsle  46166  infxrunb3rnmpt  46175  uzublem  46177  climf  46371  climf2  46413  limsupubuzlem  46459  cncficcgt0  46635  stoweidlem16  46763  stoweidlem18  46765  stoweidlem21  46768  stoweidlem29  46776  stoweidlem31  46778  stoweidlem36  46783  stoweidlem41  46788  stoweidlem44  46791  stoweidlem45  46792  stoweidlem51  46798  stoweidlem55  46802  stoweidlem59  46806  stoweidlem60  46807  issmfgelem  47516  smfpimcclem  47554  sprsymrelf  48277