Theorem raleqtrrdv 3302

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

Syntax hints:   → wi 4   = wceq 1547  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ral 3055  df-rex 3065

This theorem is referenced by:  fveqressseq  7027  prmind2  16652  symgfixf1  19410  efgsp1  19710  efgsres  19711  ablfac2  20064  cncnp  23270  prdsxmslem2  24519  cnmpopc  24920  pi1coghm  25053  dvivthlem1  26000  iblulm  26397  xrlimcnp  26957  2sqlem10  27416  usgr1e  29339  cusgrexi  29537  1hevtxdg0  29599  crctcshwlkn0lem7  29909  wlkiswwlksupgr2  29970  wwlksnext  29986  clwwlkccatlem  30084  clwlkclwwlklem2a1  30087  clwlkclwwlkf1lem3  30101  wwlksext2clwwlk  30152  wwlksubclwwlk  30153  clwwlknonex2  30204  1wlkdlem4  30235  fnpreimac  32769  selvply1rhmlemb  33710  eulerpartlemsv3  34552  bnj1514  35252  exidreslem  38245  exidresid  38247  sticksstones11  42642  lpirlnr  43563  oaun3lem1  43820  fourierdlem73  46623  linds0  48957