Theorem ralbid 3275

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077

This theorem is used by:  raleqbid  3343  sbcralt  3818  sbcrext  3819  riota5f  7405  zfrep6OLD  7967  cnfcom3clem  9709  cplem2  9955  cplem2OLD  9956  infxpenc2lem2  10102  acnlem  10130  lble  12272  fsuppmapnn0fiubex  14138  nosupbnd1  28076  noinfbnd1  28091  chirred  33002  rspc2daf  33110  aciunf1lem  33303  srepdflem2  36005  indexa  38760  riotasvd  40106  cdlemk36  42063  modelaxreplem3  46063  choicefi  46307  axccdom  46328  rexabsle  46522  infxrunb3rnmpt  46531  uzublem  46533  climf  46727  climf2  46769  limsupubuzlem  46815  cncficcgt0  46991  stoweidlem16  47119  stoweidlem18  47121  stoweidlem21  47124  stoweidlem29  47132  stoweidlem31  47134  stoweidlem36  47139  stoweidlem41  47144  stoweidlem44  47147  stoweidlem45  47148  stoweidlem51  47154  stoweidlem55  47158  stoweidlem59  47162  stoweidlem60  47163  issmfgelem  47872  smfpimcclem  47910  sprsymrelf  48670