Theorem ralbid 3279

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-ral 3068

This theorem is referenced by:  raleqbid  3364  sbcralt  3894  sbcrext  3895  riota5f  7433  zfrep6  7995  cnfcom3clem  9774  cplem2  9959  infxpenc2lem2  10089  acnlem  10117  lble  12247  fsuppmapnn0fiubex  14043  nosupbnd1  27777  noinfbnd1  27792  chirred  32427  rspc2daf  32495  aciunf1lem  32680  indexa  37693  riotasvd  38912  cdlemk36  40870  choicefi  45107  axccdom  45129  rexabsle  45334  infxrunb3rnmpt  45343  uzublem  45345  climf  45543  climf2  45587  limsupubuzlem  45633  cncficcgt0  45809  stoweidlem16  45937  stoweidlem18  45939  stoweidlem21  45942  stoweidlem29  45950  stoweidlem31  45952  stoweidlem36  45957  stoweidlem41  45962  stoweidlem44  45965  stoweidlem45  45966  stoweidlem51  45972  stoweidlem55  45976  stoweidlem59  45980  stoweidlem60  45981  issmfgelem  46690  smfpimcclem  46728  sprsymrelf  47369