Theorem raleqtrrdv 3303

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

Syntax hints:   → wi 4   = wceq 1540  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  fveqressseq  7051  prmind2  16655  symgfixf1  19367  efgsp1  19667  efgsres  19668  ablfac2  20021  cncnp  23167  prdsxmslem2  24417  cnmpopc  24822  pi1coghm  24961  dvivthlem1  25913  iblulm  26316  xrlimcnp  26878  2sqlem10  27339  usgr1e  29172  cusgrexi  29370  1hevtxdg0  29433  crctcshwlkn0lem7  29746  wlkiswwlksupgr2  29807  wwlksnext  29823  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwlkclwwlkf1lem3  29935  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwlknonex2  30038  1wlkdlem4  30069  fnpreimac  32595  eulerpartlemsv3  34352  bnj1514  35053  exidreslem  37871  exidresid  37873  sticksstones11  42144  lpirlnr  43106  oaun3lem1  43363  fourierdlem73  46177  linds0  48451