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  4769  cbvfo  5991  isoselem  6026  ofrfval  6311  issmo2  6560  smoeq  6561  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  nninfisollem0  7470  isacnm  7559  fzrevral2  10513  fzrevral3  10514  fzshftral  10515  fzoshftral  10657  zsupcllemstep  10662  zsupcllemex  10663  infssuzex  10666  suprzubdc  10671  nninfdcex  10672  uzsinds  10881  iseqf1olemqk  10944  seq3f1olemstep  10951  seq3f1olemp  10952  eqs1  11396  swrdspsleq  11439  pfxeq  11468  pfxsuffeqwrdeq  11470  caucvgre  11747  cvg1nlemres  11751  rexuz3  11756  resqrexlemoverl  11787  resqrexlemsqa  11790  resqrexlemex  11791  climconst  12056  climshftlemg  12068  serf0  12118  summodclem2  12149  summodc  12150  zsumdc  12151  mertenslemi1  12302  prodmodclem2  12344  prodmodc  12345  zproddc  12346  prmind2  12898  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemnn0  13313  ennnfonelemr  13314  grpidpropdg  13694  sgrppropd  13728  mndpropd  13753  nmznsg  14016  ghmnsgima  14071  cmnpropd  14098  rngpropd  14254  ringpropd  14343  lsspropdg  14768  isridlrng  14819  isassa  15002  assapropd  15014  mplvalcoe  15081  lmfval  15294  lmconst  15317  cncnp  15331  metss  15595  sin0pilem2  15883  fsumdvdsmul  16105  2sqlem10  16244  usgruspgrben  16427  wlkeq  16595  wlkl1loop  16599  uspgr2wlkeq  16606  upgr2wlkdc  16618  clwwlkccatlem  16641  clwwlknp  16658  clwwlkn1  16659  clwwlkn2  16662  nninfsellemdc  17053  nninfself  17056  nninfsellemeqinf  17059  nninfomni  17062