Theorem raleqtrrdv 3298

Description: Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)

Hypotheses

Ref	Expression
raleqtrrdv.1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
raleqtrrdv.2	⊢ (𝜑 → 𝐵 = 𝐴)

Assertion

Ref	Expression
raleqtrrdv	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem raleqtrrdv

Step	Hyp	Ref	Expression
1		raleqtrrdv.1	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		raleqtrrdv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
3	2	raleqdv 3294	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   = wceq 1541  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ral 3050  df-rex 3059

This theorem is referenced by:  fveqressseq  7021  prmind2  16606  symgfixf1  19359  efgsp1  19659  efgsres  19660  ablfac2  20013  cncnp  23205  prdsxmslem2  24454  cnmpopc  24859  pi1coghm  24998  dvivthlem1  25950  iblulm  26353  xrlimcnp  26915  2sqlem10  27376  usgr1e  29234  cusgrexi  29432  1hevtxdg0  29495  crctcshwlkn0lem7  29805  wlkiswwlksupgr2  29866  wwlksnext  29882  clwwlkccatlem  29980  clwlkclwwlklem2a1  29983  clwlkclwwlkf1lem3  29997  wwlksext2clwwlk  30048  wwlksubclwwlk  30049  clwwlknonex2  30100  1wlkdlem4  30131  fnpreimac  32664  eulerpartlemsv3  34385  bnj1514  35086  exidreslem  37927  exidresid  37929  sticksstones11  42259  lpirlnr  43224  oaun3lem1  43481  fourierdlem73  46291  linds0  48580