Theorem ralbid 3269

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1784   ∈ wcel 2105  ∀wral 3060

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 1912  ax-6 1970  ax-7 2010  ax-12 2170

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

This theorem is referenced by:  raleqbid  3351  sbcralt  3866  sbcrext  3867  riota5f  7397  zfrep6  7945  cnfcom3clem  9704  cplem2  9889  infxpenc2lem2  10019  acnlem  10047  lble  12171  fsuppmapnn0fiubex  13962  nosupbnd1  27454  noinfbnd1  27469  chirred  31916  rspc2daf  31976  aciunf1lem  32155  indexa  36905  riotasvd  38130  cdlemk36  40088  choicefi  44198  axccdom  44220  rexabsle  44428  infxrunb3rnmpt  44437  uzublem  44439  climf  44637  climf2  44681  limsupubuzlem  44727  cncficcgt0  44903  stoweidlem16  45031  stoweidlem18  45033  stoweidlem21  45036  stoweidlem29  45044  stoweidlem31  45046  stoweidlem36  45051  stoweidlem41  45056  stoweidlem44  45059  stoweidlem45  45060  stoweidlem51  45066  stoweidlem55  45070  stoweidlem59  45074  stoweidlem60  45075  issmfgelem  45784  smfpimcclem  45822  sprsymrelf  46462