Theorem ralbida 3143

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)

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	pm5.74da 804	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
4	1, 3	albid 2222	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)))
5		df-ral 3056	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
6		df-ral 3056	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  Ⅎwnf 1791   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-nf 1792  df-ral 3056

This theorem is referenced by:  ralbid  3144  2ralbida  3145  ac6num  10058  neiptopreu  21984  istrkg2ld  26505  funcnv5mpt  30679  xrralrecnnge  42544  climf2  42825  clim2f2  42829  limsupub  42863  climinfmpt  42874  limsupubuzmpt  42878  limsupre2mpt  42889  limsupre3mpt  42893  limsupreuzmpt  42898  xlimmnfmpt  43002  xlimpnfmpt  43003  smfsupmpt  43963  smfinfmpt  43967