Theorem ralbid 3277

Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3187. (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 3275	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

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

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 2215

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

This theorem is used by:  raleqbid  3345  sbcralt  3822  sbcrext  3823  riota5f  7402  zfrep6OLD  7956  cnfcom3clem  9688  cplem2  9895  cplem2OLD  9896  infxpenc2lem2  10027  acnlem  10055  lble  12195  fsuppmapnn0fiubex  14060  nosupbnd1  27958  noinfbnd1  27973  chirred  32884  rspc2daf  32950  aciunf1lem  33143  indexa  38491  riotasvd  39837  cdlemk36  41794  modelaxreplem3  45811  choicefi  46039  axccdom  46060  rexabsle  46255  infxrunb3rnmpt  46264  uzublem  46266  climf  46460  climf2  46502  limsupubuzlem  46548  cncficcgt0  46724  stoweidlem16  46852  stoweidlem18  46854  stoweidlem21  46857  stoweidlem29  46865  stoweidlem31  46867  stoweidlem36  46872  stoweidlem41  46877  stoweidlem44  46880  stoweidlem45  46881  stoweidlem51  46887  stoweidlem55  46891  stoweidlem59  46895  stoweidlem60  46896  issmfgelem  47605  smfpimcclem  47643  sprsymrelf  48403