Theorem raleqtrrdv 3294

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 3290	. 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  7017  prmind2  16614  symgfixf1  19334  efgsp1  19634  efgsres  19635  ablfac2  19988  cncnp  23183  prdsxmslem2  24433  cnmpopc  24838  pi1coghm  24977  dvivthlem1  25929  iblulm  26332  xrlimcnp  26894  2sqlem10  27355  usgr1e  29208  cusgrexi  29406  1hevtxdg0  29469  crctcshwlkn0lem7  29779  wlkiswwlksupgr2  29840  wwlksnext  29856  clwwlkccatlem  29951  clwlkclwwlklem2a1  29954  clwlkclwwlkf1lem3  29968  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  clwwlknonex2  30071  1wlkdlem4  30102  fnpreimac  32628  eulerpartlemsv3  34328  bnj1514  35029  exidreslem  37856  exidresid  37858  sticksstones11  42129  lpirlnr  43090  oaun3lem1  43347  fourierdlem73  46161  linds0  48438