Theorem raleqtrrdv 3323

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

Syntax hints:   → wi 4   = wceq 1559  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ral 3076  df-rex 3086

This theorem is referenced by:  fveqressseq  7054  prmind2  16700  symgfixf1  19458  efgsp1  19758  efgsres  19759  ablfac2  20112  cncnp  23318  prdsxmslem2  24567  cnmpopc  24968  pi1coghm  25101  dvivthlem1  26048  iblulm  26445  xrlimcnp  27008  2sqlem10  27467  usgr1e  29390  cusgrexi  29588  1hevtxdg0  29650  crctcshwlkn0lem7  29960  wlkiswwlksupgr2  30021  wwlksnext  30037  clwwlkccatlem  30135  clwlkclwwlklem2a1  30138  clwlkclwwlkf1lem3  30152  wwlksext2clwwlk  30203  wwlksubclwwlk  30204  clwwlknonex2  30255  1wlkdlem4  30286  fnpreimac  32820  selvply1rhmlemb  33775  eulerpartlemsv3  34617  bnj1514  35320  exidreslem  38329  exidresid  38331  sticksstones11  42726  lpirlnr  43647  oaun3lem1  43904  fourierdlem73  46706  linds0  49040