Theorem raleqdv 3326

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ral 3062  df-rex 3071

This theorem is referenced by:  raleqtrdv  3328  raleqtrrdv  3330  raleqbidva  3332  raleleqOLD  3343  raldifeq  4494  frpoinsg  6364  wfisgOLD  6375  f12dfv  7293  f13dfv  7294  cbvfo  7309  isoselem  7361  ofrfvalg  7705  omsinds  7908  frpoins3xpg  8165  frpoins3xp3g  8166  frrlem4  8314  wfrlem4OLD  8352  issmo2  8389  smoeq  8390  on2ind  8707  on3ind  8708  naddsuc2  8739  frfi  9321  marypha1lem  9473  marypha1  9474  dfoi  9551  oieq2  9553  ordtypecbv  9557  ordtypelem2  9559  ordtypelem3  9560  ordtypelem9  9566  wemapwe  9737  ttrclss  9760  ttrclselem2  9766  frinsg  9791  tcrank  9924  isacn  10084  pwsdompw  10243  isfin2  10334  isfin3ds  10369  isf33lem  10406  hsmexlem4  10469  zorn2lem6  10541  zorn2lem7  10542  zorn2g  10543  fpwwe2lem12  10682  uzsupss  12982  fzrevral2  13653  fzrevral3  13654  fzshftral  13655  fzoshftral  13823  uzsinds  14028  expmulnbnd  14274  eqs1  14650  swrdspsleq  14703  pfxeq  14734  pfxsuffeqwrdeq  14736  repswsymballbi  14818  cshw1  14860  pfx2  14986  wwlktovf1  14996  eqwrds3  15000  rexuz3  15387  rexuzre  15391  limsupgle  15513  rlim  15531  climconst  15579  rlimclim1  15581  climshftlem  15610  isercoll  15704  caucvgb  15716  serf0  15717  mertenslem1  15920  coprmprod  16698  coprmproddvds  16700  prmind2  16722  vdwlem10  17028  vdwlem13  17031  vdwnnlem2  17034  vdwnnlem3  17035  vdwnn  17036  ramval  17046  ramz  17063  prmgaplem5  17093  isacs  17694  cidpropd  17753  monpropd  17781  isssc  17864  fullsubc  17895  funcpropd  17947  isfth  17961  fthpropd  17968  grpidpropd  18675  sgrppropd  18744  mndpropd  18772  nmznsg  19186  ghmnsgima  19258  symgextfo  19440  gsmsymgrfixlem1  19445  gsmsymgrfix  19446  fvcosymgeq  19447  gsmsymgreqlem2  19449  psgnunilem3  19514  sylow2blem3  19640  sylow3lem6  19650  cmnpropd  19809  telgsumfzs  20007  rngpropd  20171  ringpropd  20285  c0snmgmhm  20462  abvpropd  20836  lsspropd  21016  lmhmpropd  21072  lbspropd  21098  pj1lmhm  21099  psgndiflemB  21618  phlpropd  21673  islindf  21832  lindfmm  21847  islindf4  21858  islindf5  21859  assapropd  21892  scmatf1  22537  isclo  23095  lmfval  23240  lmconst  23269  iscnrm2  23346  ist0-2  23352  ist1-2  23355  ishaus2  23359  subislly  23489  elpt  23580  elptr  23581  ptbasfi  23589  fclscmp  24038  ufilcmp  24040  cnpfcf  24049  alexsubALTlem1  24055  alexsubALTlem2  24056  alexsubALTlem4  24058  tmdgsum2  24104  tsmsf1o  24153  ustval  24211  ucnval  24286  imasdsf1olem  24383  imasf1oxmet  24385  imasf1omet  24386  metss  24521  prdsxmslem2  24542  lebnumlem3  24995  ishtpy  25004  lmnn  25297  evthicc  25494  cniccbdd  25496  ovolicc2lem4  25555  0pledm  25708  cniccibl  25876  cnicciblnc  25878  c1lip1  26036  lhop1  26053  itgsubstlem  26089  ulmshftlem  26432  ulm0  26434  ulmcau  26438  rlimcnp  27008  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  chtub  27256  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  pntpbnd  27632  pntibndlem2  27635  pntibndlem3  27636  pntibnd  27637  pntlemi  27648  pntleme  27652  pntlem3  27653  pntlemp  27654  pntleml  27655  pnt3  27656  madebdaylemlrcut  27937  noinds  27978  no2indslem  27987  no3inds  27991  precsexlem9  28239  istrkgld  28467  trgcgrg  28523  tgcgr4  28539  isperp  28720  brbtwn  28914  usgruspgrb  29200  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nbgr1vtx  29375  uvtx01vtx  29414  cplgr1v  29447  wlkeq  29652  wlkl1loop  29656  uspgr2wlkeq  29664  upgr2wlk  29686  redwlk  29690  wlkp1lem8  29698  usgr2wlkneq  29776  usgr2trlncl  29780  usgr2pthlem  29783  usgr2pth  29784  pthdlem1  29786  uspgrn2crct  29828  crctcshwlkn0  29841  wwlknp  29863  wwlksn0s  29881  wlkiswwlks1  29887  wlkiswwlks2lem4  29892  wwlksnred  29912  rusgrnumwwlkl1  29988  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a  30017  clwlkclwwlklem3  30020  clwwlkn  30045  clwwlknp  30056  clwwlkinwwlk  30059  clwwlkn1  30060  clwwlkn2  30063  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  1ewlk  30134  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  dfconngr1  30207  isconngr1  30209  frgr3v  30294  frgrwopregasn  30335  frgrwopregbsn  30336  ubth  30892  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1  32673  fnpreimac  32681  crngmxidl  33497  lmxrge0  33951  measval  34199  isrnmeas  34201  sitgval  34334  eulerpartlemo  34367  eulerpartlemn  34383  subfacp1lem3  35187  subfacp1lem5  35189  txpconn  35237  cvxpconn  35247  cvmscbv  35263  cvmsi  35270  cvmsval  35271  satf  35358  sat1el2xp  35384  elmrsubrn  35525  weiunlem2  36464  bj-raldifsn  37101  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  heicant  37662  mblfinlem3  37666  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  sdclem1  37750  fdc  37752  rrncmslem  37839  isass  37853  isrngod  37905  isgrpda  37962  iscom2  38002  pautsetN  40100  tendofset  40760  tendoset  40761  hdmap14lem13  41882  3factsumint1  42022  sticksstones3  42149  kelac1  43075  gicabl  43111  cantnfresb  43337  safesnsupfilb  43431  fiinfi  43586  clsk1independent  44059  scotteqd  44256  wessf1ornlem  45190  uzub  45442  rexanuz2nf  45503  mccl  45613  climsuse  45623  limsupmnfuzlem  45741  limsupmnfuz  45742  limsupre3uzlem  45750  limsupre3uz  45751  limsupreuz  45752  0cnv  45757  climuz  45759  lmbr3  45762  limsupgt  45793  liminflt  45820  xlimpnfxnegmnf  45829  xlimmnf  45856  xlimpnf  45857  xlimmnfmpt  45858  xlimpnfmpt  45859  dfxlim2  45863  fourierdlem2  46124  fourierdlem3  46125  fourierdlem31  46153  fourierdlem47  46168  fourierdlem70  46191  fourierdlem71  46192  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  etransclem48  46297  etransc  46298  caragenval  46508  omessle  46513  smfmullem2  46807  smfmul  46810  2ffzoeq  47339  iccpval  47402  iccpartigtl  47410  cycl3grtrilem  47913  grlimgrtri  47963  grilcbri2  47971  usgrexmpl2trifr  47996  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  lindsrng01  48385  rrx2line  48661  fucofulem2  49006  thincpropd  49091