Theorem raleqtrrdv 3325

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ral 3079  df-rex 3089

This theorem is used by:  fveqressseq  7076  prmind2  16781  symgfixf1  19570  efgsp1  19870  efgsres  19871  ablfac2  20224  cncnp  23511  prdsxmslem2  24761  cnmpopc  25162  pi1coghm  25295  dvivthlem1  26242  iblulm  26650  xrlimcnp  27213  2sqlem10  27672  usgr1e  29713  cusgrexi  29911  1hevtxdg0  29973  crctcshwlkn0lem7  30292  wlkiswwlksupgr2  30353  wwlksnext  30369  clwwlkccatlem  30467  clwlkclwwlklem2a1  30470  clwlkclwwlkf1lem3  30484  wwlksext2clwwlk  30535  wwlksubclwwlk  30536  clwwlknonex2  30587  1wlkdlem4  30618  fnpreimac  33151  selvply1rhmlemb  34037  eulerpartlemsv3  34880  bnj1514  35580  exidreslem  38635  exidresid  38637  sticksstones11  43030  lpirlnr  43966  oaun3lem1  44223  fourierdlem73  47015  linds0  49403