Theorem raleqdv 2755

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  raleqtrdv  2757  raleqtrrdv  2759  raleqbidv  2765  raleqbidva  2767  omsinds  4771  cbvfo  5994  isoselem  6029  ofrfval  6315  issmo2  6564  smoeq  6565  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  nninfisollem0  7476  isacnm  7565  fzrevral2  10530  fzrevral3  10531  fzshftral  10532  fzoshftral  10674  zsupcllemstep  10679  zsupcllemex  10680  infssuzex  10683  suprzubdc  10688  nninfdcex  10689  uzsinds  10902  iseqf1olemqk  10965  seq3f1olemstep  10972  seq3f1olemp  10973  eqs1  11418  swrdspsleq  11461  pfxeq  11490  pfxsuffeqwrdeq  11492  caucvgre  11769  cvg1nlemres  11773  rexuz3  11778  resqrexlemoverl  11809  resqrexlemsqa  11812  resqrexlemex  11813  climconst  12081  climshftlemg  12093  serf0  12143  summodclem2  12174  summodc  12175  zsumdc  12176  mertenslemi1  12327  prodmodclem2  12369  prodmodc  12370  zproddc  12371  prmind2  12923  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemnn0  13371  ennnfonelemr  13372  grpidpropdg  13753  sgrppropd  13787  mndpropd  13812  nmznsg  14075  ghmnsgima  14130  cmnpropd  14188  rngpropd  14361  ringpropd  14450  lsspropdg  14877  isridlrng  14928  isassa  15111  assapropd  15123  mplvalcoe  15206  lmfval  15419  lmconst  15442  cncnp  15456  metss  15720  sin0pilem2  16009  fsumdvdsmul  16285  chtqub  16296  2sqlem10  16449  usgruspgrben  16632  wlkeq  16800  wlkl1loop  16804  uspgr2wlkeq  16811  upgr2wlkdc  16823  clwwlkccatlem  16846  clwwlknp  16863  clwwlkn1  16864  clwwlkn2  16867  nninfsellemdc  17259  nninfself  17262  nninfsellemeqinf  17265  nninfomni  17268