Theorem raleqdv 3319

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2721  df-ral 3055  df-rex 3064

This theorem is referenced by:  raleqtrdv  3321  raleqtrrdv  3323  raleqbidva  3325  raleleqOLD  3336  raldifeq  4499  frpoinsg  6358  wfisgOLD  6369  f12dfv  7289  f13dfv  7290  cbvfo  7305  isoselem  7356  ofrfvalg  7700  omsinds  7902  omsindsOLD  7903  frpoins3xpg  8159  frpoins3xp3g  8160  frrlem4  8308  wfrlem4OLD  8346  issmo2  8383  smoeq  8384  on2ind  8703  on3ind  8704  frfi  9324  marypha1lem  9477  marypha1  9478  dfoi  9555  oieq2  9557  ordtypecbv  9561  ordtypelem2  9563  ordtypelem3  9564  ordtypelem9  9570  wemapwe  9741  ttrclss  9764  ttrclselem2  9770  frinsg  9795  tcrank  9928  isacn  10088  pwsdompw  10247  isfin2  10338  isfin3ds  10373  isf33lem  10410  hsmexlem4  10473  zorn2lem6  10545  zorn2lem7  10546  zorn2g  10547  fpwwe2lem12  10686  uzsupss  12980  fzrevral2  13645  fzrevral3  13646  fzshftral  13647  fzoshftral  13808  uzsinds  14012  expmulnbnd  14258  eqs1  14633  swrdspsleq  14686  pfxeq  14717  pfxsuffeqwrdeq  14719  repswsymballbi  14801  cshw1  14843  pfx2  14969  wwlktovf1  14979  eqwrds3  14983  rexuz3  15366  rexuzre  15370  limsupgle  15492  rlim  15510  climconst  15558  rlimclim1  15560  climshftlem  15589  isercoll  15685  caucvgb  15697  serf0  15698  mertenslem1  15901  coprmprod  16675  coprmproddvds  16677  prmind2  16699  vdwlem10  17005  vdwlem13  17008  vdwnnlem2  17011  vdwnnlem3  17012  vdwnn  17013  ramval  17023  ramz  17040  prmgaplem5  17070  isacs  17677  cidpropd  17736  monpropd  17766  isssc  17849  fullsubc  17882  funcpropd  17935  isfth  17949  fthpropd  17956  grpidpropd  18668  sgrppropd  18737  mndpropd  18765  nmznsg  19176  ghmnsgima  19248  symgextfo  19432  gsmsymgrfixlem1  19437  gsmsymgrfix  19438  fvcosymgeq  19439  gsmsymgreqlem2  19441  psgnunilem3  19506  sylow2blem3  19632  sylow3lem6  19642  cmnpropd  19801  telgsumfzs  19999  rngpropd  20169  ringpropd  20279  c0snmgmhm  20456  abvpropd  20826  lsspropd  21007  lmhmpropd  21063  lbspropd  21089  pj1lmhm  21090  psgndiflemB  21609  phlpropd  21664  islindf  21823  lindfmm  21838  islindf4  21849  islindf5  21850  assapropd  21882  scmatf1  22524  isclo  23082  lmfval  23227  lmconst  23256  iscnrm2  23333  ist0-2  23339  ist1-2  23342  ishaus2  23346  subislly  23476  elpt  23567  elptr  23568  ptbasfi  23576  fclscmp  24025  ufilcmp  24027  cnpfcf  24036  alexsubALTlem1  24042  alexsubALTlem2  24043  alexsubALTlem4  24045  tmdgsum2  24091  tsmsf1o  24140  ustval  24198  ucnval  24273  imasdsf1olem  24370  imasf1oxmet  24372  imasf1omet  24373  metss  24508  prdsxmslem2  24529  lebnumlem3  24980  ishtpy  24989  lmnn  25282  evthicc  25479  cniccbdd  25481  ovolicc2lem4  25540  0pledm  25693  cniccibl  25861  cnicciblnc  25863  c1lip1  26021  lhop1  26038  itgsubstlem  26074  ulmshftlem  26415  ulm0  26417  ulmcau  26421  rlimcnp  26990  fsumdvdsmul  27220  fsumdvdsmulOLD  27222  chtub  27238  2sqlem10  27454  dchrisum0flb  27536  pntpbnd1  27612  pntpbnd  27614  pntibndlem2  27617  pntibndlem3  27618  pntibnd  27619  pntlemi  27630  pntleme  27634  pntlem3  27635  pntlemp  27636  pntleml  27637  pnt3  27638  madebdaylemlrcut  27919  noinds  27956  no2indslem  27965  no3inds  27969  precsexlem9  28211  istrkgld  28383  trgcgrg  28439  tgcgr4  28455  isperp  28636  brbtwn  28830  usgruspgrb  29116  nbgr2vtx1edg  29283  nbuhgr2vtx1edgb  29285  nbgr1vtx  29291  uvtx01vtx  29330  cplgr1v  29363  wlkeq  29568  wlkl1loop  29572  uspgr2wlkeq  29580  upgr2wlk  29602  redwlk  29606  wlkp1lem8  29614  usgr2wlkneq  29690  usgr2trlncl  29694  usgr2pthlem  29697  usgr2pth  29698  pthdlem1  29700  uspgrn2crct  29739  crctcshwlkn0  29752  wwlknp  29774  wwlksn0s  29792  wlkiswwlks1  29798  wlkiswwlks2lem4  29803  wwlksnred  29823  rusgrnumwwlkl1  29899  clwwlkccatlem  29919  clwlkclwwlklem2a1  29922  clwlkclwwlklem2a  29928  clwlkclwwlklem3  29931  clwwlkn  29956  clwwlknp  29967  clwwlkinwwlk  29970  clwwlkn1  29971  clwwlkn2  29974  clwwlkel  29976  clwwlkf  29977  clwwlkwwlksb  29984  1ewlk  30045  upgr3v3e3cycl  30110  upgr4cycl4dv4e  30115  dfconngr1  30118  isconngr1  30120  frgr3v  30205  frgrwopregasn  30246  frgrwopregbsn  30247  ubth  30803  acunirnmpt2  32578  acunirnmpt2f  32579  aciunf1  32581  fnpreimac  32589  crngmxidl  33362  lmxrge0  33798  measval  34062  isrnmeas  34064  sitgval  34197  eulerpartlemo  34230  eulerpartlemn  34246  subfacp1lem3  35050  subfacp1lem5  35052  txpconn  35100  cvxpconn  35110  cvmscbv  35126  cvmsi  35133  cvmsval  35134  satf  35221  sat1el2xp  35247  elmrsubrn  35388  bj-raldifsn  36847  poimirlem26  37387  poimirlem27  37388  poimirlem31  37392  poimirlem32  37393  heicant  37396  mblfinlem3  37400  ovoliunnfl  37403  voliunnfl  37405  volsupnfl  37406  sdclem1  37484  fdc  37486  rrncmslem  37573  isass  37587  isrngod  37639  isgrpda  37696  iscom2  37736  pautsetN  39837  tendofset  40497  tendoset  40498  hdmap14lem13  41619  3factsumint1  41760  sticksstones3  41887  kelac1  42791  gicabl  42827  cantnfresb  43057  naddsuc2  43126  safesnsupfilb  43152  fiinfi  43307  clsk1independent  43780  scotteqd  43978  wessf1ornlem  44858  uzub  45112  rexanuz2nf  45174  mccl  45285  climsuse  45295  limsupmnfuzlem  45413  limsupmnfuz  45414  limsupre3uzlem  45422  limsupre3uz  45423  limsupreuz  45424  0cnv  45429  climuz  45431  lmbr3  45434  limsupgt  45465  liminflt  45492  xlimpnfxnegmnf  45501  xlimmnf  45528  xlimpnf  45529  xlimmnfmpt  45530  xlimpnfmpt  45531  dfxlim2  45535  fourierdlem2  45796  fourierdlem3  45797  fourierdlem31  45825  fourierdlem47  45840  fourierdlem70  45863  fourierdlem71  45864  fourierdlem80  45873  fourierdlem103  45896  fourierdlem104  45897  fourierdlem113  45906  etransclem48  45969  etransc  45970  caragenval  46180  omessle  46185  smfmullem2  46479  smfmul  46482  2ffzoeq  47006  iccpval  47053  iccpartigtl  47061  grilcbri2  47568  lindsrng01  47928  rrx2line  48205