Theorem ralbid 3245

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3048

This theorem is referenced by:  raleqbid  3324  sbcralt  3818  sbcrext  3819  riota5f  7331  zfrep6  7887  cnfcom3clem  9595  cplem2  9783  infxpenc2lem2  9911  acnlem  9939  lble  12074  fsuppmapnn0fiubex  13899  nosupbnd1  27653  noinfbnd1  27668  chirred  32375  rspc2daf  32445  aciunf1lem  32644  indexa  37772  riotasvd  39054  cdlemk36  41011  modelaxreplem3  45072  choicefi  45296  axccdom  45318  rexabsle  45516  infxrunb3rnmpt  45525  uzublem  45527  climf  45721  climf2  45763  limsupubuzlem  45809  cncficcgt0  45985  stoweidlem16  46113  stoweidlem18  46115  stoweidlem21  46118  stoweidlem29  46126  stoweidlem31  46128  stoweidlem36  46133  stoweidlem41  46138  stoweidlem44  46141  stoweidlem45  46142  stoweidlem51  46148  stoweidlem55  46152  stoweidlem59  46156  stoweidlem60  46157  issmfgelem  46866  smfpimcclem  46904  sprsymrelf  47594