Theorem raleqdv 2708

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ∀wral 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  raleqtrdv  2710  raleqtrrdv  2712  raleqbidv  2718  raleqbidva  2720  omsinds  4671  cbvfo  5856  isoselem  5891  ofrfval  6169  issmo2  6377  smoeq  6378  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  nninfisollem0  7234  isacnm  7317  fzrevral2  10230  fzrevral3  10231  fzshftral  10232  fzoshftral  10369  zsupcllemstep  10374  zsupcllemex  10375  infssuzex  10378  suprzubdc  10381  nninfdcex  10382  uzsinds  10591  iseqf1olemqk  10654  seq3f1olemstep  10661  seq3f1olemp  10662  eqs1  11085  swrdspsleq  11123  pfxeq  11150  pfxsuffeqwrdeq  11152  caucvgre  11325  cvg1nlemres  11329  rexuz3  11334  resqrexlemoverl  11365  resqrexlemsqa  11368  resqrexlemex  11369  climconst  11634  climshftlemg  11646  serf0  11696  summodclem2  11726  summodc  11727  zsumdc  11728  mertenslemi1  11879  prodmodclem2  11921  prodmodc  11922  zproddc  11923  prmind2  12475  ennnfoneleminc  12815  ennnfonelemex  12818  ennnfonelemnn0  12826  ennnfonelemr  12827  grpidpropdg  13239  sgrppropd  13278  mndpropd  13305  nmznsg  13582  ghmnsgima  13637  cmnpropd  13664  rngpropd  13750  ringpropd  13833  lsspropdg  14226  isridlrng  14277  mplvalcoe  14485  lmfval  14697  lmconst  14721  cncnp  14735  metss  14999  sin0pilem2  15287  fsumdvdsmul  15496  2sqlem10  15635  nninfsellemdc  15984  nninfself  15987  nninfsellemeqinf  15990  nninfomni  15993