Theorem raleqdv 3299

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqtrdv  3301  raleqtrrdv  3303  raleqbidva  3305  raleleqOLD  3316  raldifeq  4457  frpoinsg  6316  f12dfv  7248  f13dfv  7249  cbvfo  7264  isoselem  7316  ofrfvalg  7661  omsinds  7863  frpoins3xpg  8119  frpoins3xp3g  8120  frrlem4  8268  issmo2  8318  smoeq  8319  on2ind  8633  on3ind  8634  naddsuc2  8665  frfi  9232  marypha1lem  9384  marypha1  9385  dfoi  9464  oieq2  9466  ordtypecbv  9470  ordtypelem2  9472  ordtypelem3  9473  ordtypelem9  9479  wemapwe  9650  ttrclss  9673  ttrclselem2  9679  frinsg  9704  tcrank  9837  isacn  9997  pwsdompw  10156  isfin2  10247  isfin3ds  10282  isf33lem  10319  hsmexlem4  10382  zorn2lem6  10454  zorn2lem7  10455  zorn2g  10456  fpwwe2lem12  10595  uzsupss  12899  fzrevral2  13574  fzrevral3  13575  fzshftral  13576  fzoshftral  13745  uzsinds  13952  expmulnbnd  14200  eqs1  14577  swrdspsleq  14630  pfxeq  14661  pfxsuffeqwrdeq  14663  repswsymballbi  14745  cshw1  14787  pfx2  14913  wwlktovf1  14923  eqwrds3  14927  rexuz3  15315  rexuzre  15319  limsupgle  15443  rlim  15461  climconst  15509  rlimclim1  15511  climshftlem  15540  isercoll  15634  caucvgb  15646  serf0  15647  mertenslem1  15850  coprmprod  16631  coprmproddvds  16633  prmind2  16655  vdwlem10  16961  vdwlem13  16964  vdwnnlem2  16967  vdwnnlem3  16968  vdwnn  16969  ramval  16979  ramz  16996  prmgaplem5  17026  isacs  17612  cidpropd  17671  monpropd  17699  isssc  17782  fullsubc  17812  funcpropd  17864  isfth  17878  fthpropd  17885  grpidpropd  18589  sgrppropd  18658  mndpropd  18686  nmznsg  19100  ghmnsgima  19172  symgextfo  19352  gsmsymgrfixlem1  19357  gsmsymgrfix  19358  fvcosymgeq  19359  gsmsymgreqlem2  19361  psgnunilem3  19426  sylow2blem3  19552  sylow3lem6  19562  cmnpropd  19721  telgsumfzs  19919  rngpropd  20083  ringpropd  20197  c0snmgmhm  20371  abvpropd  20744  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  pj1lmhm  21007  psgndiflemB  21509  phlpropd  21564  islindf  21721  lindfmm  21736  islindf4  21747  islindf5  21748  assapropd  21781  scmatf1  22418  isclo  22974  lmfval  23119  lmconst  23148  iscnrm2  23225  ist0-2  23231  ist1-2  23234  ishaus2  23238  subislly  23368  elpt  23459  elptr  23460  ptbasfi  23468  fclscmp  23917  ufilcmp  23919  cnpfcf  23928  alexsubALTlem1  23934  alexsubALTlem2  23935  alexsubALTlem4  23937  tmdgsum2  23983  tsmsf1o  24032  ustval  24090  ucnval  24164  imasdsf1olem  24261  imasf1oxmet  24263  imasf1omet  24264  metss  24396  prdsxmslem2  24417  lebnumlem3  24862  ishtpy  24871  lmnn  25163  evthicc  25360  cniccbdd  25362  ovolicc2lem4  25421  0pledm  25574  cniccibl  25742  cnicciblnc  25744  c1lip1  25902  lhop1  25919  itgsubstlem  25955  ulmshftlem  26298  ulm0  26300  ulmcau  26304  rlimcnp  26875  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  chtub  27123  2sqlem10  27339  dchrisum0flb  27421  pntpbnd1  27497  pntpbnd  27499  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemi  27515  pntleme  27519  pntlem3  27520  pntlemp  27521  pntleml  27522  pnt3  27523  madebdaylemlrcut  27810  noinds  27852  no2indslem  27861  no3inds  27865  precsexlem9  28117  istrkgld  28386  trgcgrg  28442  tgcgr4  28458  isperp  28639  brbtwn  28826  usgruspgrb  29110  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nbgr1vtx  29285  uvtx01vtx  29324  cplgr1v  29357  wlkeq  29562  wlkl1loop  29566  uspgr2wlkeq  29574  upgr2wlk  29596  redwlk  29600  wlkp1lem8  29608  usgr2wlkneq  29686  usgr2trlncl  29690  usgr2pthlem  29693  usgr2pth  29694  pthdlem1  29696  uspgrn2crct  29738  crctcshwlkn0  29751  wwlknp  29773  wwlksn0s  29791  wlkiswwlks1  29797  wlkiswwlks2lem4  29802  wwlksnred  29822  rusgrnumwwlkl1  29898  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwwlkn  29955  clwwlknp  29966  clwwlkinwwlk  29969  clwwlkn1  29970  clwwlkn2  29973  clwwlkel  29975  clwwlkf  29976  clwwlkwwlksb  29983  1ewlk  30044  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  dfconngr1  30117  isconngr1  30119  frgr3v  30204  frgrwopregasn  30245  frgrwopregbsn  30246  ubth  30802  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1  32587  fnpreimac  32595  fxpgaval  33124  crngmxidl  33440  lmxrge0  33942  measval  34188  isrnmeas  34190  sitgval  34323  eulerpartlemo  34356  eulerpartlemn  34372  onvf1odlem4  35093  subfacp1lem3  35169  subfacp1lem5  35171  txpconn  35219  cvxpconn  35229  cvmscbv  35245  cvmsi  35252  cvmsval  35253  satf  35340  sat1el2xp  35366  elmrsubrn  35507  weiunlem2  36451  bj-raldifsn  37088  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  heicant  37649  mblfinlem3  37653  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  sdclem1  37737  fdc  37739  rrncmslem  37826  isass  37840  isrngod  37892  isgrpda  37949  iscom2  37989  pautsetN  40092  tendofset  40752  tendoset  40753  hdmap14lem13  41874  3factsumint1  42009  sticksstones3  42136  kelac1  43052  gicabl  43088  cantnfresb  43313  safesnsupfilb  43407  fiinfi  43562  clsk1independent  44035  scotteqd  44226  wessf1ornlem  45179  uzub  45427  rexanuz2nf  45488  mccl  45596  climsuse  45606  limsupmnfuzlem  45724  limsupmnfuz  45725  limsupre3uzlem  45733  limsupre3uz  45734  limsupreuz  45735  0cnv  45740  climuz  45742  lmbr3  45745  limsupgt  45776  liminflt  45803  xlimpnfxnegmnf  45812  xlimmnf  45839  xlimpnf  45840  xlimmnfmpt  45841  xlimpnfmpt  45842  dfxlim2  45846  fourierdlem2  46107  fourierdlem3  46108  fourierdlem31  46136  fourierdlem47  46151  fourierdlem70  46174  fourierdlem71  46175  fourierdlem80  46184  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  etransclem48  46280  etransc  46281  caragenval  46491  omessle  46496  smfmullem2  46790  smfmul  46793  2ffzoeq  47328  iccpval  47416  iccpartigtl  47424  cycl3grtrilem  47945  grlimgrtri  47995  grilcbri2  48003  usgrexmpl2trifr  48028  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  lindsrng01  48457  rrx2line  48729  initopropd  49232  termopropd  49233  fucofulem2  49300  thincpropd  49431  isinito2lem  49487