Theorem raleqdv 3323

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
raleqdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleqdv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		raleq 3320	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ral 3059  df-rex 3068

This theorem is referenced by:  raleqtrdv  3325  raleqtrrdv  3327  raleqbidva  3329  raleleqOLD  3340  raldifeq  4499  frpoinsg  6365  wfisgOLD  6376  f12dfv  7292  f13dfv  7293  cbvfo  7308  isoselem  7360  ofrfvalg  7704  omsinds  7907  omsindsOLD  7908  frpoins3xpg  8163  frpoins3xp3g  8164  frrlem4  8312  wfrlem4OLD  8350  issmo2  8387  smoeq  8388  on2ind  8705  on3ind  8706  naddsuc2  8737  frfi  9318  marypha1lem  9470  marypha1  9471  dfoi  9548  oieq2  9550  ordtypecbv  9554  ordtypelem2  9556  ordtypelem3  9557  ordtypelem9  9563  wemapwe  9734  ttrclss  9757  ttrclselem2  9763  frinsg  9788  tcrank  9921  isacn  10081  pwsdompw  10240  isfin2  10331  isfin3ds  10366  isf33lem  10403  hsmexlem4  10466  zorn2lem6  10538  zorn2lem7  10539  zorn2g  10540  fpwwe2lem12  10679  uzsupss  12979  fzrevral2  13649  fzrevral3  13650  fzshftral  13651  fzoshftral  13819  uzsinds  14024  expmulnbnd  14270  eqs1  14646  swrdspsleq  14699  pfxeq  14730  pfxsuffeqwrdeq  14732  repswsymballbi  14814  cshw1  14856  pfx2  14982  wwlktovf1  14992  eqwrds3  14996  rexuz3  15383  rexuzre  15387  limsupgle  15509  rlim  15527  climconst  15575  rlimclim1  15577  climshftlem  15606  isercoll  15700  caucvgb  15712  serf0  15713  mertenslem1  15916  coprmprod  16694  coprmproddvds  16696  prmind2  16718  vdwlem10  17023  vdwlem13  17026  vdwnnlem2  17029  vdwnnlem3  17030  vdwnn  17031  ramval  17041  ramz  17058  prmgaplem5  17088  isacs  17695  cidpropd  17754  monpropd  17784  isssc  17867  fullsubc  17900  funcpropd  17953  isfth  17967  fthpropd  17974  grpidpropd  18687  sgrppropd  18756  mndpropd  18784  nmznsg  19198  ghmnsgima  19270  symgextfo  19454  gsmsymgrfixlem1  19459  gsmsymgrfix  19460  fvcosymgeq  19461  gsmsymgreqlem2  19463  psgnunilem3  19528  sylow2blem3  19654  sylow3lem6  19664  cmnpropd  19823  telgsumfzs  20021  rngpropd  20191  ringpropd  20301  c0snmgmhm  20478  abvpropd  20852  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  pj1lmhm  21116  psgndiflemB  21635  phlpropd  21690  islindf  21849  lindfmm  21864  islindf4  21875  islindf5  21876  assapropd  21909  scmatf1  22552  isclo  23110  lmfval  23255  lmconst  23284  iscnrm2  23361  ist0-2  23367  ist1-2  23370  ishaus2  23374  subislly  23504  elpt  23595  elptr  23596  ptbasfi  23604  fclscmp  24053  ufilcmp  24055  cnpfcf  24064  alexsubALTlem1  24070  alexsubALTlem2  24071  alexsubALTlem4  24073  tmdgsum2  24119  tsmsf1o  24168  ustval  24226  ucnval  24301  imasdsf1olem  24398  imasf1oxmet  24400  imasf1omet  24401  metss  24536  prdsxmslem2  24557  lebnumlem3  25008  ishtpy  25017  lmnn  25310  evthicc  25507  cniccbdd  25509  ovolicc2lem4  25568  0pledm  25721  cniccibl  25890  cnicciblnc  25892  c1lip1  26050  lhop1  26067  itgsubstlem  26103  ulmshftlem  26446  ulm0  26448  ulmcau  26452  rlimcnp  27022  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  chtub  27270  2sqlem10  27486  dchrisum0flb  27568  pntpbnd1  27644  pntpbnd  27646  pntibndlem2  27649  pntibndlem3  27650  pntibnd  27651  pntlemi  27662  pntleme  27666  pntlem3  27667  pntlemp  27668  pntleml  27669  pnt3  27670  madebdaylemlrcut  27951  noinds  27992  no2indslem  28001  no3inds  28005  precsexlem9  28253  istrkgld  28481  trgcgrg  28537  tgcgr4  28553  isperp  28734  brbtwn  28928  usgruspgrb  29214  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nbgr1vtx  29389  uvtx01vtx  29428  cplgr1v  29461  wlkeq  29666  wlkl1loop  29670  uspgr2wlkeq  29678  upgr2wlk  29700  redwlk  29704  wlkp1lem8  29712  usgr2wlkneq  29788  usgr2trlncl  29792  usgr2pthlem  29795  usgr2pth  29796  pthdlem1  29798  uspgrn2crct  29837  crctcshwlkn0  29850  wwlknp  29872  wwlksn0s  29890  wlkiswwlks1  29896  wlkiswwlks2lem4  29901  wwlksnred  29921  rusgrnumwwlkl1  29997  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a  30026  clwlkclwwlklem3  30029  clwwlkn  30054  clwwlknp  30065  clwwlkinwwlk  30068  clwwlkn1  30069  clwwlkn2  30072  clwwlkel  30074  clwwlkf  30075  clwwlkwwlksb  30082  1ewlk  30143  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  dfconngr1  30216  isconngr1  30218  frgr3v  30303  frgrwopregasn  30344  frgrwopregbsn  30345  ubth  30901  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1  32679  fnpreimac  32687  crngmxidl  33476  lmxrge0  33912  measval  34178  isrnmeas  34180  sitgval  34313  eulerpartlemo  34346  eulerpartlemn  34362  subfacp1lem3  35166  subfacp1lem5  35168  txpconn  35216  cvxpconn  35226  cvmscbv  35242  cvmsi  35249  cvmsval  35250  satf  35337  sat1el2xp  35363  elmrsubrn  35504  weiunlem2  36445  bj-raldifsn  37082  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  heicant  37641  mblfinlem3  37645  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  sdclem1  37729  fdc  37731  rrncmslem  37818  isass  37832  isrngod  37884  isgrpda  37941  iscom2  37981  pautsetN  40080  tendofset  40740  tendoset  40741  hdmap14lem13  41862  3factsumint1  42002  sticksstones3  42129  kelac1  43051  gicabl  43087  cantnfresb  43313  safesnsupfilb  43407  fiinfi  43562  clsk1independent  44035  scotteqd  44232  wessf1ornlem  45127  uzub  45380  rexanuz2nf  45442  mccl  45553  climsuse  45563  limsupmnfuzlem  45681  limsupmnfuz  45682  limsupre3uzlem  45690  limsupre3uz  45691  limsupreuz  45692  0cnv  45697  climuz  45699  lmbr3  45702  limsupgt  45733  liminflt  45760  xlimpnfxnegmnf  45769  xlimmnf  45796  xlimpnf  45797  xlimmnfmpt  45798  xlimpnfmpt  45799  dfxlim2  45803  fourierdlem2  46064  fourierdlem3  46065  fourierdlem31  46093  fourierdlem47  46108  fourierdlem70  46131  fourierdlem71  46132  fourierdlem80  46141  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  etransclem48  46237  etransc  46238  caragenval  46448  omessle  46453  smfmullem2  46747  smfmul  46750  2ffzoeq  47276  iccpval  47339  iccpartigtl  47347  grlimgrtri  47898  grilcbri2  47906  usgrexmpl2trifr  47931  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  lindsrng01  48313  rrx2line  48589