Theorem ralbid 2983

Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	ralbida 2982	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 196  Ⅎwnf 1708   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710  df-ral 2917

This theorem is referenced by:  raleqbid  3150  sbcralt  3510  sbcrext  3511  sbcrextOLD  3512  riota5f  6636  zfrep6  7134  cnfcom3clem  8602  cplem2  8753  infxpenc2lem2  8843  acnlem  8871  lble  10975  fsuppmapnn0fiubex  12792  chirred  29254  aciunf1lem  29462  nosupbnd1  31860  indexa  33528  riotasvd  34242  cdlemk36  36201  choicefi  39392  axccdom  39416  rexabsle  39646  infxrunb3rnmpt  39655  uzublem  39657  climf  39854  climf2  39898  limsupubuzlem  39944  cncficcgt0  40101  stoweidlem16  40233  stoweidlem18  40235  stoweidlem21  40238  stoweidlem29  40246  stoweidlem31  40248  stoweidlem36  40253  stoweidlem41  40258  stoweidlem44  40261  stoweidlem45  40262  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  stoweidlem60  40277  issmfgelem  40977  smfpimcclem  41013  sprsymrelf  41745