Theorem raleqdv 2635

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
raleqdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		raleq 2629	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 14	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332  ∀wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422

This theorem is referenced by:  raleqbidv  2641  raleqbidva  2643  omsinds  4543  cbvfo  5694  isoselem  5729  ofrfval  5998  issmo2  6194  smoeq  6195  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  fzrevral2  9917  fzrevral3  9918  fzshftral  9919  fzoshftral  10046  uzsinds  10246  iseqf1olemqk  10298  seq3f1olemstep  10305  seq3f1olemp  10306  caucvgre  10785  cvg1nlemres  10789  rexuz3  10794  resqrexlemoverl  10825  resqrexlemsqa  10828  resqrexlemex  10829  climconst  11091  climshftlemg  11103  serf0  11153  summodclem2  11183  summodc  11184  zsumdc  11185  mertenslemi1  11336  prodmodclem2  11378  prodmodc  11379  zproddc  11380  zsupcllemstep  11674  zsupcllemex  11675  infssuzex  11678  prmind2  11837  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemnn0  11971  ennnfonelemr  11972  lmfval  12400  lmconst  12424  cncnp  12438  metss  12702  sin0pilem2  12911  nninfsellemdc  13381  nninfself  13384  nninfsellemeqinf  13387  nninfomni  13390