Theorem raleqdv 3329

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ral 3086  df-rex 3096

This theorem is referenced by:  raleqtrdv  3331  raleqtrrdv  3333  raleqbidva  3335  raldifeq  4457  frpoinsg  6345  f12dfv  7272  f13dfv  7273  cbvfo  7288  isoselem  7340  ofrfvalg  7683  omsinds  7883  frpoins3xpg  8136  frpoins3xp3g  8137  frrlem4  8286  issmo2  8336  smoeq  8337  on2ind  8655  on3ind  8656  naddsuc2  8688  frfi  9245  marypha1lem  9393  marypha1  9394  dfoi  9473  oieq2  9475  ordtypecbv  9479  ordtypelem2  9481  ordtypelem3  9482  ordtypelem9  9488  wemapwe  9666  ttrclss  9689  ttrclselem2  9695  frinsg  9723  tcrank  9856  scotteqd  9863  isacn  10028  pwsdompw  10186  isfin2  10278  isfin3ds  10313  isf33lem  10350  hsmexlem4  10413  zorn2lem6  10485  zorn2lem7  10486  zorn2g  10487  fpwwe2lem12  10627  uzsupss  12964  fzrevral2  13641  fzrevral3  13642  fzshftral  13643  fzoshftral  13816  uzsinds  14023  expmulnbnd  14271  eqs1  14650  swrdspsleq  14703  pfxeq  14733  pfxsuffeqwrdeq  14735  repswsymballbi  14817  cshw1  14859  pfx2  14984  wwlktovf1  14994  eqwrds3  14998  rexuz3  15400  rexuzre  15404  limsupgle  15528  rlim  15546  climconst  15594  rlimclim1  15596  climshftlem  15625  isercoll  15719  caucvgb  15731  serf0  15732  mertenslem1  15938  coprmprod  16719  coprmproddvds  16721  prmind2  16743  vdwlem10  17050  vdwlem13  17053  vdwnnlem2  17056  vdwnnlem3  17057  vdwnn  17058  ramval  17068  ramz  17085  prmgaplem5  17115  isacs  17707  cidpropd  17766  monpropd  17794  isssc  17877  fullsubc  17907  funcpropd  17959  isfth  17973  fthpropd  17980  grpidpropd  18720  sgrppropd  18789  mndpropd  18817  nmznsg  19234  ghmnsgima  19310  symgextfo  19492  gsmsymgrfixlem1  19497  gsmsymgrfix  19498  fvcosymgeq  19499  gsmsymgreqlem2  19501  psgnunilem3  19566  sylow2blem3  19692  sylow3lem6  19702  cmnpropd  19861  telgsumfzs  20059  rngpropd  20252  ringpropd  20371  c0snmgmhm  20544  abvpropd  20916  lsspropd  21116  lmhmpropd  21172  lbspropd  21198  pj1lmhm  21199  psgndiflemB  21719  phlpropd  21774  islindf  21931  lindfmm  21946  islindf4  21957  islindf5  21958  assapropd  21990  scmatf1  22657  isclo  23213  lmfval  23358  lmconst  23387  iscnrm2  23464  ist0-2  23470  ist1-2  23473  ishaus2  23477  subislly  23607  elpt  23698  elptr  23699  ptbasfi  23707  fclscmp  24156  ufilcmp  24158  cnpfcf  24167  alexsubALTlem1  24173  alexsubALTlem2  24174  alexsubALTlem4  24176  tmdgsum2  24222  tsmsf1o  24271  ustval  24329  ucnval  24402  imasdsf1olem  24499  imasf1oxmet  24501  imasf1omet  24502  metss  24634  prdsxmslem2  24655  lebnumlem3  25091  ishtpy  25100  lmnn  25391  evthicc  25587  cniccbdd  25589  ovolicc2lem4  25648  0pledm  25801  cniccibl  25969  cnicciblnc  25971  c1lip1  26125  lhop1  26142  itgsubstlem  26176  ulmshftlem  26518  ulm0  26520  ulmcau  26524  rlimcnp  27096  fsumdvdsmul  27325  chtub  27342  2sqlem10  27558  dchrisum0flb  27640  pntpbnd1  27716  pntpbnd  27718  pntibndlem2  27721  pntibndlem3  27722  pntibnd  27723  pntlemi  27734  pntleme  27738  pntlem3  27739  pntlemp  27740  pntleml  27741  pnt3  27742  madebdaylemlrcut  28058  noinds  28104  no2indlesm  28113  no3inds  28117  precsexlem9  28374  istrkgld  28694  trgcgrg  28750  tgcgr4  28766  isperp  28951  brbtwn  29190  usgruspgrb  29474  nbgr2vtx1edg  29641  nbuhgr2vtx1edgb  29643  nbgr1vtx  29649  uvtx01vtx  29688  cplgr1v  29721  wlkeq  29924  wlkl1loop  29928  uspgr2wlkeq  29936  upgr2wlk  29957  redwlk  29961  wlkp1lem8  29969  usgr2wlkneq  30046  usgr2trlncl  30050  usgr2pthlem  30053  usgr2pth  30054  pthdlem1  30056  uspgrn2crct  30098  crctcshwlkn0  30111  wwlknp  30133  wwlksn0s  30151  wlkiswwlks1  30157  wlkiswwlks2lem4  30162  wwlksnred  30182  rusgrnumwwlkl1  30261  clwwlkccatlem  30281  clwlkclwwlklem2a1  30284  clwlkclwwlklem2a  30290  clwlkclwwlklem3  30293  clwwlkn  30318  clwwlknp  30329  clwwlkinwwlk  30332  clwwlkn1  30333  clwwlkn2  30336  clwwlkel  30338  clwwlkf  30339  clwwlkwwlksb  30346  1ewlk  30407  upgr3v3e3cycl  30472  upgr4cycl4dv4e  30477  dfconngr1  30480  isconngr1  30482  frgr3v  30567  frgrwopregasn  30608  frgrwopregbsn  30609  ubth  31166  acunirnmpt2  32946  acunirnmpt2f  32947  aciunf1  32949  fnpreimac  32956  fxpgaval  33428  crngmxidl  33697  lmxrge0  34287  measval  34533  isrnmeas  34535  sitgval  34667  eulerpartlemo  34700  eulerpartlemn  34716  onvf1odlem4  35523  subfacp1lem3  35607  subfacp1lem5  35609  txpconn  35657  cvxpconn  35667  cvmscbv  35683  cvmsi  35690  cvmsval  35691  satf  35778  sat1el2xp  35804  elmrsubrn  35945  weiunlem  36897  bj-raldifsn  37665  poimirlem26  38220  poimirlem27  38221  poimirlem31  38225  poimirlem32  38226  heicant  38229  mblfinlem3  38233  ovoliunnfl  38236  voliunnfl  38238  volsupnfl  38239  sdclem1  38317  fdc  38319  rrncmslem  38406  isass  38420  isrngod  38472  isgrpda  38529  iscom2  38569  pautsetN  40797  tendofset  41457  tendoset  41458  hdmap14lem13  42579  3factsumint1  42713  sticksstones3  42840  kelac1  43717  gicabl  43753  cantnfresb  43978  safesnsupfilb  44071  fiinfi  44226  clsk1independent  44699  wessf1ornlem  45830  uzub  46072  rexanuz2nf  46133  mccl  46241  climsuse  46251  limsupmnfuzlem  46367  limsupmnfuz  46368  limsupre3uzlem  46376  limsupre3uz  46377  limsupreuz  46378  0cnv  46383  climuz  46385  lmbr3  46388  limsupgt  46419  liminflt  46446  xlimpnfxnegmnf  46455  xlimmnf  46482  xlimpnf  46483  xlimmnfmpt  46484  xlimpnfmpt  46485  dfxlim2  46489  fourierdlem2  46750  fourierdlem3  46751  fourierdlem31  46779  fourierdlem47  46794  fourierdlem70  46817  fourierdlem71  46818  fourierdlem80  46827  fourierdlem103  46850  fourierdlem104  46851  fourierdlem113  46860  etransclem48  46923  etransc  46924  caragenval  47134  omessle  47139  smfmullem2  47433  smfmul  47436  2ffzoeq  47989  iccpval  48088  iccpartigtl  48096  nprmmul1  48200  cycl3grtrilem  48635  grlimedgclnbgr  48684  grlimgrtri  48692  grilcbri2  48700  usgrexmpl2trifr  48726  gpg5nbgrvtx03star  48769  gpg5nbgr3star  48770  lindsrng01  49168  rrx2line  49440  initopropd  49941  termopropd  49942  fucofulem2  50009  thincpropd  50140  isinito2lem  50196