Theorem raleqbidva 3354

Description: Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypotheses

Ref	Expression
raleqbidva.1	⊢ (𝜑 → 𝐴 = 𝐵)
raleqbidva.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem raleqbidva

Step	Hyp	Ref	Expression
1		raleqbidva.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	ralbidva 3111	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
3		raleqbidva.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	raleqdv 3348	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 278	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ral 3069

This theorem is referenced by:  catpropd  17418  cidpropd  17419  funcpropd  17616  fullpropd  17636  natpropd  17694  gsumpropd2lem  18363  istrkgc  26815  istrkgb  26816  istrkgcb  26817  istrkge  26818  iscgrg  26873  isperp  27073  clwlkclwwlk  28366  rngurd  31482  lindfpropd  31576  ist0cld  31783  matunitlindflem1  35773  sticksstones3  40104  sticksstones11  40112