Theorem raleqtrrdv 3294

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

Syntax hints:   → wi 4   = wceq 1541  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-ral 3046  df-rex 3055

This theorem is referenced by:  fveqressseq  7007  prmind2  16588  symgfixf1  19342  efgsp1  19642  efgsres  19643  ablfac2  19996  cncnp  23188  prdsxmslem2  24437  cnmpopc  24842  pi1coghm  24981  dvivthlem1  25933  iblulm  26336  xrlimcnp  26898  2sqlem10  27359  usgr1e  29216  cusgrexi  29414  1hevtxdg0  29477  crctcshwlkn0lem7  29787  wlkiswwlksupgr2  29848  wwlksnext  29864  clwwlkccatlem  29959  clwlkclwwlklem2a1  29962  clwlkclwwlkf1lem3  29976  wwlksext2clwwlk  30027  wwlksubclwwlk  30028  clwwlknonex2  30079  1wlkdlem4  30110  fnpreimac  32643  eulerpartlemsv3  34364  bnj1514  35065  exidreslem  37896  exidresid  37898  sticksstones11  42168  lpirlnr  43129  oaun3lem1  43386  fourierdlem73  46196  linds0  48476