Theorem raleqdv 2736

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ∀wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  raleqtrdv  2738  raleqtrrdv  2740  raleqbidv  2746  raleqbidva  2748  omsinds  4720  cbvfo  5926  isoselem  5961  ofrfval  6244  issmo2  6455  smoeq  6456  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nninfisollem0  7329  isacnm  7418  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzoshftral  10485  zsupcllemstep  10490  zsupcllemex  10491  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  uzsinds  10707  iseqf1olemqk  10770  seq3f1olemstep  10777  seq3f1olemp  10778  eqs1  11206  swrdspsleq  11249  pfxeq  11278  pfxsuffeqwrdeq  11280  caucvgre  11543  cvg1nlemres  11547  rexuz3  11552  resqrexlemoverl  11583  resqrexlemsqa  11586  resqrexlemex  11587  climconst  11852  climshftlemg  11864  serf0  11914  summodclem2  11945  summodc  11946  zsumdc  11947  mertenslemi1  12098  prodmodclem2  12140  prodmodc  12141  zproddc  12142  prmind2  12694  ennnfoneleminc  13034  ennnfonelemex  13037  ennnfonelemnn0  13045  ennnfonelemr  13046  grpidpropdg  13459  sgrppropd  13498  mndpropd  13525  nmznsg  13802  ghmnsgima  13857  cmnpropd  13884  rngpropd  13971  ringpropd  14054  lsspropdg  14448  isridlrng  14499  mplvalcoe  14707  lmfval  14920  lmconst  14943  cncnp  14957  metss  15221  sin0pilem2  15509  fsumdvdsmul  15718  2sqlem10  15857  usgruspgrben  16040  wlkeq  16208  wlkl1loop  16212  uspgr2wlkeq  16219  upgr2wlkdc  16231  clwwlkccatlem  16254  clwwlknp  16271  clwwlkn1  16272  clwwlkn2  16275  nninfsellemdc  16633  nninfself  16636  nninfsellemeqinf  16639  nninfomni  16642