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 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   = wceq 1568  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-ral 3078  df-rex 3088

This theorem is referenced by:  fveqressseq  7074  prmind2  16742  symgfixf1  19506  efgsp1  19806  efgsres  19807  ablfac2  20160  cncnp  23416  prdsxmslem2  24665  cnmpopc  25066  pi1coghm  25199  dvivthlem1  26146  iblulm  26546  xrlimcnp  27109  2sqlem10  27568  usgr1e  29561  cusgrexi  29759  1hevtxdg0  29821  crctcshwlkn0lem7  30131  wlkiswwlksupgr2  30192  wwlksnext  30208  clwwlkccatlem  30306  clwlkclwwlklem2a1  30309  clwlkclwwlkf1lem3  30323  wwlksext2clwwlk  30374  wwlksubclwwlk  30375  clwwlknonex2  30426  1wlkdlem4  30457  fnpreimac  32981  selvply1rhmlemb  33875  eulerpartlemsv3  34717  bnj1514  35417  exidreslem  38494  exidresid  38496  sticksstones11  42891  lpirlnr  43814  oaun3lem1  44071  fourierdlem73  46863  linds0  49212