Theorem raleqtrrdv 3327

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ral 3081  df-rex 3091

This theorem is used by:  fveqressseq  7103  prmind2  16889  symgfixf1  19681  efgsp1  19981  efgsres  19982  ablfac2  20335  cncnp  23628  prdsxmslem2  24878  cnmpopc  25279  pi1coghm  25412  dvivthlem1  26358  iblulm  26764  xrlimcnp  27326  2sqlem10  27785  usgr1e  29856  cusgrexi  30054  1hevtxdg0  30116  crctcshwlkn0lem7  30435  wlkiswwlksupgr2  30496  wwlksnext  30512  clwwlkccatlem  30610  clwlkclwwlklem2a1  30613  clwlkclwwlkf1lem3  30627  wwlksext2clwwlk  30678  wwlksubclwwlk  30679  clwwlknonex2  30730  1wlkdlem4  30761  fnpreimac  33336  selvply1rhmlemb  34221  eulerpartlemsv3  35063  bnj1514  35763  exidreslem  39003  exidresid  39005  sticksstones11  43398  lpirlnr  44311  oaun3lem1  44568  fourierdlem73  47394  linds0  49782