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  16860  symgfixf1  19651  efgsp1  19951  efgsres  19952  ablfac2  20305  cncnp  23598  prdsxmslem2  24848  cnmpopc  25249  pi1coghm  25382  dvivthlem1  26328  iblulm  26734  xrlimcnp  27296  2sqlem10  27755  usgr1e  29826  cusgrexi  30024  1hevtxdg0  30086  crctcshwlkn0lem7  30405  wlkiswwlksupgr2  30466  wwlksnext  30482  clwwlkccatlem  30580  clwlkclwwlklem2a1  30583  clwlkclwwlkf1lem3  30597  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  clwwlknonex2  30700  1wlkdlem4  30731  fnpreimac  33306  selvply1rhmlemb  34193  eulerpartlemsv3  35035  bnj1514  35735  exidreslem  38854  exidresid  38856  sticksstones11  43249  lpirlnr  44162  oaun3lem1  44419  fourierdlem73  47232  linds0  49620