Theorem raleqdv 2590

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 2584	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 14	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299  ∀wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380

This theorem is referenced by:  raleqbidv  2596  raleqbidva  2598  omsinds  4473  cbvfo  5618  isoselem  5653  ofrfval  5922  issmo2  6116  smoeq  6117  tfrlemisucaccv  6152  tfr1onlemsucaccv  6168  tfrcllemsucaccv  6181  fzrevral2  9727  fzrevral3  9728  fzshftral  9729  fzoshftral  9856  uzsinds  10056  iseqf1olemqk  10108  seq3f1olemstep  10115  seq3f1olemp  10116  caucvgre  10593  cvg1nlemres  10597  rexuz3  10602  resqrexlemoverl  10633  resqrexlemsqa  10636  resqrexlemex  10637  climconst  10898  climshftlemg  10910  serf0  10960  summodclem2  10990  summodc  10991  zsumdc  10992  mertenslemi1  11143  zsupcllemstep  11433  zsupcllemex  11434  infssuzex  11437  prmind2  11594  ennnfoneleminc  11716  ennnfonelemex  11719  ennnfonelemnn0  11727  ennnfonelemr  11728  lmfval  12143  lmconst  12166  cncnp  12180  metss  12422  ellimc3ap  12511  nninfsellemdc  12790  nninfself  12793  nninfsellemeqinf  12796  nninfomni  12799