Theorem raleqtrrdv 3313

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ral 3053  df-rex 3062

This theorem is referenced by:  fveqressseq  7074  prmind2  16709  symgfixf1  19423  efgsp1  19723  efgsres  19724  ablfac2  20077  cncnp  23223  prdsxmslem2  24473  cnmpopc  24878  pi1coghm  25017  dvivthlem1  25970  iblulm  26373  xrlimcnp  26935  2sqlem10  27396  usgr1e  29229  cusgrexi  29427  1hevtxdg0  29490  crctcshwlkn0lem7  29803  wlkiswwlksupgr2  29864  wwlksnext  29880  clwwlkccatlem  29975  clwlkclwwlklem2a1  29978  clwlkclwwlkf1lem3  29992  wwlksext2clwwlk  30043  wwlksubclwwlk  30044  clwwlknonex2  30095  1wlkdlem4  30126  fnpreimac  32654  eulerpartlemsv3  34398  bnj1514  35099  exidreslem  37906  exidresid  37908  sticksstones11  42174  lpirlnr  43108  oaun3lem1  43365  fourierdlem73  46175  linds0  48408