Theorem raleqtrrdv 3302

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 3298	. 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 3063

This theorem is referenced by:  fveqressseq  7033  prmind2  16624  symgfixf1  19378  efgsp1  19678  efgsres  19679  ablfac2  20032  cncnp  23236  prdsxmslem2  24485  cnmpopc  24890  pi1coghm  25029  dvivthlem1  25981  iblulm  26384  xrlimcnp  26946  2sqlem10  27407  usgr1e  29330  cusgrexi  29528  1hevtxdg0  29591  crctcshwlkn0lem7  29901  wlkiswwlksupgr2  29962  wwlksnext  29978  clwwlkccatlem  30076  clwlkclwwlklem2a1  30079  clwlkclwwlkf1lem3  30093  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  clwwlknonex2  30196  1wlkdlem4  30227  fnpreimac  32759  eulerpartlemsv3  34538  bnj1514  35238  exidreslem  38117  exidresid  38119  sticksstones11  42515  lpirlnr  43463  oaun3lem1  43720  fourierdlem73  46526  linds0  48814