Theorem raleqtrrdv 3338

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

Syntax hints:   → wi 4   = wceq 1537  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ral 3068  df-rex 3077

This theorem is referenced by:  fveqressseq  7113  prmind2  16732  symgfixf1  19479  efgsp1  19779  efgsres  19780  ablfac2  20133  cncnp  23309  prdsxmslem2  24563  cnmpopc  24974  pi1coghm  25113  dvivthlem1  26067  iblulm  26468  xrlimcnp  27029  2sqlem10  27490  usgr1e  29280  cusgrexi  29478  1hevtxdg0  29541  crctcshwlkn0lem7  29849  wlkiswwlksupgr2  29910  wwlksnext  29926  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlkf1lem3  30038  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwlknonex2  30141  1wlkdlem4  30172  fnpreimac  32689  eulerpartlemsv3  34326  bnj1514  35039  exidreslem  37837  exidresid  37839  sticksstones11  42113  lpirlnr  43074  oaun3lem1  43336  fourierdlem73  46100  linds0  48194