Theorem ralbida 3277

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)

Hypotheses

Ref	Expression
ralbida.1	⊢ Ⅎ𝑥𝜑
ralbida.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbida	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Proof of Theorem ralbida

Step	Hyp	Ref	Expression
1		ralbida.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		ralbida.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	biimpd 232	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
4	1, 3	ralimdaa 3267	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
5	2	biimprd 251	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓))
6	1, 5	ralimdaa 3267	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓))
7	4, 6	impbid 215	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081

This theorem is used by:  ralbid  3279  2ralbida  3289  naddsuc2  8736  ac6num  10581  neiptopreu  23478  istrkg2ld  28949  funcnv5mpt  33330  nadd1suc  44584  xrralrecnnge  46604  climf2  46879  clim2f2  46883  limsupub  46917  climinfmpt  46928  limsupubuzmpt  46932  limsupre2mpt  46943  limsupre3mpt  46947  limsupreuzmpt  46952  xlimmnfmpt  47056  xlimpnfmpt  47057  smfsupmpt  48028  smfinfmpt  48032