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  7032  prmind2  16654  symgfixf1  19412  efgsp1  19712  efgsres  19713  ablfac2  20066  cncnp  23245  prdsxmslem2  24494  cnmpopc  24895  pi1coghm  25028  dvivthlem1  25975  iblulm  26372  xrlimcnp  26932  2sqlem10  27391  usgr1e  29314  cusgrexi  29512  1hevtxdg0  29574  crctcshwlkn0lem7  29884  wlkiswwlksupgr2  29945  wwlksnext  29961  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlkf1lem3  30076  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwlknonex2  30179  1wlkdlem4  30210  fnpreimac  32743  eulerpartlemsv3  34505  bnj1514  35205  exidreslem  38198  exidresid  38200  sticksstones11  42595  lpirlnr  43545  oaun3lem1  43802  fourierdlem73  46607  linds0  48935