Theorem ralbida 3240

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 3230	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
5	2	biimprd 248	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓))
6	1, 5	ralimdaa 3230	. 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  3242  2ralbida  3252  naddsuc2  8619  ac6num  10373  neiptopreu  23018  istrkg2ld  28405  funcnv5mpt  32612  nadd1suc  43375  xrralrecnnge  45379  climf2  45657  clim2f2  45661  limsupub  45695  climinfmpt  45706  limsupubuzmpt  45710  limsupre2mpt  45721  limsupre3mpt  45725  limsupreuzmpt  45730  xlimmnfmpt  45834  xlimpnfmpt  45835  smfsupmpt  46806  smfinfmpt  46810