Theorem ralbid 3158

Description: Formula-building rule for restricted universal quantifier (deduction form). (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 3156	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-ral 3068

This theorem is referenced by:  raleqbid  3343  sbcralt  3801  sbcrext  3802  riota5f  7241  zfrep6  7771  cnfcom3clem  9393  cplem2  9579  infxpenc2lem2  9707  acnlem  9735  lble  11857  fsuppmapnn0fiubex  13640  chirred  30658  rspc2daf  30717  aciunf1lem  30901  nosupbnd1  33844  noinfbnd1  33859  indexa  35818  riotasvd  36897  cdlemk36  38854  choicefi  42629  axccdom  42651  rexabsle  42849  infxrunb3rnmpt  42858  uzublem  42860  climf  43053  climf2  43097  limsupubuzlem  43143  cncficcgt0  43319  stoweidlem16  43447  stoweidlem18  43449  stoweidlem21  43452  stoweidlem29  43460  stoweidlem31  43462  stoweidlem36  43467  stoweidlem41  43472  stoweidlem44  43475  stoweidlem45  43476  stoweidlem51  43482  stoweidlem55  43486  stoweidlem59  43490  stoweidlem60  43491  issmfgelem  44191  smfpimcclem  44227  sprsymrelf  44835