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

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

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 2213

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

This theorem is used by:  raleqbid  3344  sbcralt  3819  sbcrext  3820  riota5f  7397  zfrep6OLD  7956  cnfcom3clem  9690  cplem2  9933  cplem2OLD  9934  infxpenc2lem2  10080  acnlem  10108  lble  12250  fsuppmapnn0fiubex  14115  nosupbnd1  28053  noinfbnd1  28068  chirred  32979  rspc2daf  33045  aciunf1lem  33238  indexa  38635  riotasvd  39981  cdlemk36  41938  modelaxreplem3  45922  choicefi  46157  axccdom  46178  rexabsle  46373  infxrunb3rnmpt  46382  uzublem  46384  climf  46578  climf2  46620  limsupubuzlem  46666  cncficcgt0  46842  stoweidlem16  46970  stoweidlem18  46972  stoweidlem21  46975  stoweidlem29  46983  stoweidlem31  46985  stoweidlem36  46990  stoweidlem41  46995  stoweidlem44  46998  stoweidlem45  46999  stoweidlem51  47005  stoweidlem55  47009  stoweidlem59  47013  stoweidlem60  47014  issmfgelem  47723  smfpimcclem  47761  sprsymrelf  48521