Theorem raleqtrrdv 3300

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ral 3052  df-rex 3061

This theorem is referenced by:  fveqressseq  7024  prmind2  16612  symgfixf1  19366  efgsp1  19666  efgsres  19667  ablfac2  20020  cncnp  23224  prdsxmslem2  24473  cnmpopc  24878  pi1coghm  25017  dvivthlem1  25969  iblulm  26372  xrlimcnp  26934  2sqlem10  27395  usgr1e  29318  cusgrexi  29516  1hevtxdg0  29579  crctcshwlkn0lem7  29889  wlkiswwlksupgr2  29950  wwlksnext  29966  clwwlkccatlem  30064  clwlkclwwlklem2a1  30067  clwlkclwwlkf1lem3  30081  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  clwwlknonex2  30184  1wlkdlem4  30215  fnpreimac  32749  eulerpartlemsv3  34518  bnj1514  35219  exidreslem  38078  exidresid  38080  sticksstones11  42410  lpirlnr  43359  oaun3lem1  43616  fourierdlem73  46423  linds0  48711