Theorem ralbida 3248

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 229	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
4	1, 3	ralimdaa 3238	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
5	2	biimprd 248	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓))
6	1, 5	ralimdaa 3238	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓))
7	4, 6	impbid 212	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045

This theorem is referenced by:  ralbid  3250  2ralbida  3260  naddsuc2  8665  ac6num  10432  neiptopreu  23020  istrkg2ld  28387  funcnv5mpt  32592  nadd1suc  43381  xrralrecnnge  45386  climf2  45664  clim2f2  45668  limsupub  45702  climinfmpt  45713  limsupubuzmpt  45717  limsupre2mpt  45728  limsupre3mpt  45732  limsupreuzmpt  45737  xlimmnfmpt  45841  xlimpnfmpt  45842  smfsupmpt  46813  smfinfmpt  46817