Theorem raleqtrrdv 3324

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ral 3078  df-rex 3088

This theorem is used by:  fveqressseq  7071  prmind2  16840  symgfixf1  19631  efgsp1  19931  efgsres  19932  ablfac2  20285  cncnp  23578  prdsxmslem2  24828  cnmpopc  25229  pi1coghm  25362  dvivthlem1  26308  iblulm  26716  xrlimcnp  27278  2sqlem10  27737  usgr1e  29808  cusgrexi  30006  1hevtxdg0  30068  crctcshwlkn0lem7  30387  wlkiswwlksupgr2  30448  wwlksnext  30464  clwwlkccatlem  30562  clwlkclwwlklem2a1  30565  clwlkclwwlkf1lem3  30579  wwlksext2clwwlk  30630  wwlksubclwwlk  30631  clwwlknonex2  30682  1wlkdlem4  30713  fnpreimac  33246  selvply1rhmlemb  34133  eulerpartlemsv3  34976  bnj1514  35676  exidreslem  38779  exidresid  38781  sticksstones11  43174  lpirlnr  44077  oaun3lem1  44334  fourierdlem73  47133  linds0  49521