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 260	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  fveqressseq  7079  prmind2  16865  symgfixf1  19656  efgsp1  19956  efgsres  19957  ablfac2  20310  cncnp  23603  prdsxmslem2  24853  cnmpopc  25254  pi1coghm  25387  dvivthlem1  26333  iblulm  26739  xrlimcnp  27301  2sqlem10  27760  usgr1e  29831  cusgrexi  30029  1hevtxdg0  30091  crctcshwlkn0lem7  30410  wlkiswwlksupgr2  30471  wwlksnext  30487  clwwlkccatlem  30585  clwlkclwwlklem2a1  30588  clwlkclwwlkf1lem3  30602  wwlksext2clwwlk  30653  wwlksubclwwlk  30654  clwwlknonex2  30705  1wlkdlem4  30736  fnpreimac  33311  selvply1rhmlemb  34197  eulerpartlemsv3  35039  bnj1514  35739  exidreslem  38904  exidresid  38906  sticksstones11  43299  lpirlnr  44212  oaun3lem1  44469  fourierdlem73  47282  linds0  49670