Theorem raleqtrrdv 3327

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

Syntax hints:   → wi 4   = wceq 1563  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ral 3080  df-rex 3090

This theorem is referenced by:  fveqressseq  7064  prmind2  16733  symgfixf1  19498  efgsp1  19798  efgsres  19799  ablfac2  20152  cncnp  23398  prdsxmslem2  24647  cnmpopc  25048  pi1coghm  25181  dvivthlem1  26128  iblulm  26528  xrlimcnp  27091  2sqlem10  27550  usgr1e  29504  cusgrexi  29702  1hevtxdg0  29764  crctcshwlkn0lem7  30074  wlkiswwlksupgr2  30135  wwlksnext  30151  clwwlkccatlem  30249  clwlkclwwlklem2a1  30252  clwlkclwwlkf1lem3  30266  wwlksext2clwwlk  30317  wwlksubclwwlk  30318  clwwlknonex2  30369  1wlkdlem4  30400  fnpreimac  32927  selvply1rhmlemb  33826  eulerpartlemsv3  34668  bnj1514  35368  exidreslem  38388  exidresid  38390  sticksstones11  42785  lpirlnr  43706  oaun3lem1  43963  fourierdlem73  46751  linds0  49096