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 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  7023  prmind2  16643  symgfixf1  19401  efgsp1  19701  efgsres  19702  ablfac2  20055  cncnp  23254  prdsxmslem2  24503  cnmpopc  24904  pi1coghm  25037  dvivthlem1  25985  iblulm  26387  xrlimcnp  26949  2sqlem10  27410  usgr1e  29333  cusgrexi  29531  1hevtxdg0  29594  crctcshwlkn0lem7  29904  wlkiswwlksupgr2  29965  wwlksnext  29981  clwwlkccatlem  30079  clwlkclwwlklem2a1  30082  clwlkclwwlkf1lem3  30096  wwlksext2clwwlk  30147  wwlksubclwwlk  30148  clwwlknonex2  30199  1wlkdlem4  30230  fnpreimac  32763  eulerpartlemsv3  34526  bnj1514  35226  exidreslem  38209  exidresid  38211  sticksstones11  42606  lpirlnr  43560  oaun3lem1  43817  fourierdlem73  46622  linds0  48938