Theorem raleqdv 2734

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  raleqtrdv  2736  raleqtrrdv  2738  raleqbidv  2744  raleqbidva  2746  omsinds  4718  cbvfo  5921  isoselem  5956  ofrfval  6239  issmo2  6450  smoeq  6451  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  nninfisollem0  7320  isacnm  7408  fzrevral2  10331  fzrevral3  10332  fzshftral  10333  fzoshftral  10474  zsupcllemstep  10479  zsupcllemex  10480  infssuzex  10483  suprzubdc  10486  nninfdcex  10487  uzsinds  10696  iseqf1olemqk  10759  seq3f1olemstep  10766  seq3f1olemp  10767  eqs1  11195  swrdspsleq  11238  pfxeq  11267  pfxsuffeqwrdeq  11269  caucvgre  11532  cvg1nlemres  11536  rexuz3  11541  resqrexlemoverl  11572  resqrexlemsqa  11575  resqrexlemex  11576  climconst  11841  climshftlemg  11853  serf0  11903  summodclem2  11933  summodc  11934  zsumdc  11935  mertenslemi1  12086  prodmodclem2  12128  prodmodc  12129  zproddc  12130  prmind2  12682  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemnn0  13033  ennnfonelemr  13034  grpidpropdg  13447  sgrppropd  13486  mndpropd  13513  nmznsg  13790  ghmnsgima  13845  cmnpropd  13872  rngpropd  13958  ringpropd  14041  lsspropdg  14435  isridlrng  14486  mplvalcoe  14694  lmfval  14907  lmconst  14930  cncnp  14944  metss  15208  sin0pilem2  15496  fsumdvdsmul  15705  2sqlem10  15844  usgruspgrben  16025  wlkeq  16151  wlkl1loop  16155  uspgr2wlkeq  16162  upgr2wlkdc  16172  clwwlkccatlem  16195  clwwlknp  16212  clwwlkn1  16213  clwwlkn2  16216  nninfsellemdc  16548  nninfself  16551  nninfsellemeqinf  16554  nninfomni  16557