Theorem ralbida 3273

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

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

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 1943  ax-6 2000  ax-7 2041  ax-12 2213

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

This theorem is used by:  ralbid  3275  2ralbida  3285  naddsuc2  8697  ac6num  10506  neiptopreu  23390  istrkg2ld  28833  funcnv5mpt  33172  nadd1suc  44298  xrralrecnnge  46284  climf2  46559  clim2f2  46563  limsupub  46597  climinfmpt  46608  limsupubuzmpt  46612  limsupre2mpt  46623  limsupre3mpt  46627  limsupreuzmpt  46632  xlimmnfmpt  46736  xlimpnfmpt  46737  smfsupmpt  47708  smfinfmpt  47712