Theorem raleqtrrdv 3301

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 3297	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   = wceq 1542  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3062

This theorem is referenced by:  fveqressseq  7026  prmind2  16616  symgfixf1  19370  efgsp1  19670  efgsres  19671  ablfac2  20024  cncnp  23228  prdsxmslem2  24477  cnmpopc  24882  pi1coghm  25021  dvivthlem1  25973  iblulm  26376  xrlimcnp  26938  2sqlem10  27399  usgr1e  29301  cusgrexi  29499  1hevtxdg0  29562  crctcshwlkn0lem7  29872  wlkiswwlksupgr2  29933  wwlksnext  29949  clwwlkccatlem  30047  clwlkclwwlklem2a1  30050  clwlkclwwlkf1lem3  30064  wwlksext2clwwlk  30115  wwlksubclwwlk  30116  clwwlknonex2  30167  1wlkdlem4  30198  fnpreimac  32730  eulerpartlemsv3  34499  bnj1514  35200  exidreslem  38049  exidresid  38051  sticksstones11  42447  lpirlnr  43395  oaun3lem1  43652  fourierdlem73  46459  linds0  48747