Theorem raleqtrrdv 3330

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

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

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ral 3083  df-rex 3093

This theorem is used by:  fveqressseq  7081  prmind2  16768  symgfixf1  19532  efgsp1  19832  efgsres  19833  ablfac2  20186  cncnp  23467  prdsxmslem2  24716  cnmpopc  25117  pi1coghm  25250  dvivthlem1  26197  iblulm  26600  xrlimcnp  27163  2sqlem10  27622  usgr1e  29625  cusgrexi  29823  1hevtxdg0  29885  crctcshwlkn0lem7  30195  wlkiswwlksupgr2  30256  wwlksnext  30272  clwwlkccatlem  30370  clwlkclwwlklem2a1  30373  clwlkclwwlkf1lem3  30387  wwlksext2clwwlk  30438  wwlksubclwwlk  30439  clwwlknonex2  30490  1wlkdlem4  30521  fnpreimac  33045  selvply1rhmlemb  33933  eulerpartlemsv3  34775  bnj1514  35475  exidreslem  38561  exidresid  38563  sticksstones11  42956  lpirlnr  43877  oaun3lem1  44134  fourierdlem73  46926  linds0  49278