Theorem raleqtrrdv 3329

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

Syntax hints:   → wi 4   = wceq 1539  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ral 3061  df-rex 3070

This theorem is referenced by:  fveqressseq  7098  prmind2  16723  symgfixf1  19456  efgsp1  19756  efgsres  19757  ablfac2  20110  cncnp  23289  prdsxmslem2  24543  cnmpopc  24956  pi1coghm  25095  dvivthlem1  26048  iblulm  26451  xrlimcnp  27012  2sqlem10  27473  usgr1e  29263  cusgrexi  29461  1hevtxdg0  29524  crctcshwlkn0lem7  29837  wlkiswwlksupgr2  29898  wwlksnext  29914  clwwlkccatlem  30009  clwlkclwwlklem2a1  30012  clwlkclwwlkf1lem3  30026  wwlksext2clwwlk  30077  wwlksubclwwlk  30078  clwwlknonex2  30129  1wlkdlem4  30160  fnpreimac  32682  eulerpartlemsv3  34364  bnj1514  35078  exidreslem  37885  exidresid  37887  sticksstones11  42158  lpirlnr  43134  oaun3lem1  43392  fourierdlem73  46199  linds0  48387