Theorem raleqtrrdv 3328

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

Syntax hints:   → wi 4   = wceq 1537  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ral 3060  df-rex 3069

This theorem is referenced by:  fveqressseq  7099  prmind2  16719  symgfixf1  19470  efgsp1  19770  efgsres  19771  ablfac2  20124  cncnp  23304  prdsxmslem2  24558  cnmpopc  24969  pi1coghm  25108  dvivthlem1  26062  iblulm  26465  xrlimcnp  27026  2sqlem10  27487  usgr1e  29277  cusgrexi  29475  1hevtxdg0  29538  crctcshwlkn0lem7  29846  wlkiswwlksupgr2  29907  wwlksnext  29923  clwwlkccatlem  30018  clwlkclwwlklem2a1  30021  clwlkclwwlkf1lem3  30035  wwlksext2clwwlk  30086  wwlksubclwwlk  30087  clwwlknonex2  30138  1wlkdlem4  30169  fnpreimac  32688  eulerpartlemsv3  34343  bnj1514  35056  exidreslem  37864  exidresid  37866  sticksstones11  42138  lpirlnr  43106  oaun3lem1  43364  fourierdlem73  46135  linds0  48311