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 18	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  raleqtrdv  3321  raleqtrrdv  3323  raleqbidva  3325  raldifeq  4448  frpoinsg  6346  f12dfv  7281  f13dfv  7282  cbvfo  7297  isoselem  7349  ofrfvalg  7701  omsinds  7898  frpoins3xpg  8157  frpoins3xp3g  8158  frrlem4  8307  issmo2  8357  smoeq  8358  on2ind  8678  on3ind  8679  naddsuc2  8711  frfi  9276  marypha1lem  9425  marypha1  9426  dfoi  9505  oieq2  9507  ordtypecbv  9511  ordtypelem2  9513  ordtypelem3  9514  ordtypelem9  9520  wemapwe  9698  ttrclss  9721  ttrclselem2  9727  frinsg  9755  tcrank  9901  scotteqd  9930  isacn  10123  pwsdompw  10281  isfin2  10372  isfin3ds  10407  isf33lem  10444  hsmexlem4  10507  zorn2lem6  10579  zorn2lem7  10580  zorn2g  10581  fpwwe2lem12  10727  uzsupss  13067  fzrevral2  13747  fzrevral3  13748  fzshftral  13749  fzoshftral  13922  uzsinds  14130  expmulnbnd  14379  eqs1  14760  swrdspsleq  14815  pfxeq  14845  pfxsuffeqwrdeq  14847  repswsymballbi  14931  cshw1  14973  pfx2  15098  wwlktovf1  15110  eqwrds3  15114  rexuz3  15516  rexuzre  15520  limsupgle  15644  rlim  15662  climconst  15710  rlimclim1  15712  climshftlem  15741  isercoll  15835  caucvgb  15847  serf0  15848  mertenslem1  16053  coprmprod  16836  coprmproddvds  16838  prmind2  16860  vdwlem10  17168  vdwlem13  17171  vdwnnlem2  17174  vdwnnlem3  17175  vdwnn  17176  ramval  17186  ramz  17203  prmgaplem5  17233  isacs  17825  cidpropd  17884  monpropd  17912  isssc  17995  fullsubc  18025  funcpropd  18077  isfth  18091  fthpropd  18098  grpidpropd  18842  sgrppropd  18920  mndpropd  18951  nmznsg  19378  ghmnsgima  19454  symgextfo  19636  gsmsymgrfixlem1  19641  gsmsymgrfix  19642  fvcosymgeq  19643  gsmsymgreqlem2  19645  psgnunilem3  19710  sylow2blem3  19836  sylow3lem6  19846  cmnpropd  20005  telgsumfzs  20203  rngpropd  20396  ringpropd  20519  c0snmgmhm  20692  abvpropd  21092  lsspropd  21292  lmhmpropd  21348  lbspropd  21374  pj1lmhm  21375  psgndiflemB  21906  phlpropd  21961  islindf  22118  lindfmm  22133  islindf4  22144  islindf5  22145  assapropd  22179  scmatf1  22846  isclo  23405  lmfval  23550  lmconst  23579  iscnrm2  23656  ist0-2  23662  ist1-2  23665  ishaus2  23669  subislly  23800  elpt  23891  elptr  23892  ptbasfi  23900  fclscmp  24349  ufilcmp  24351  cnpfcf  24360  alexsubALTlem1  24366  alexsubALTlem2  24367  alexsubALTlem4  24369  tmdgsum2  24415  tsmsf1o  24464  ustval  24522  ucnval  24595  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  metss  24827  prdsxmslem2  24848  lebnumlem3  25284  ishtpy  25293  lmnn  25584  evthicc  25780  cniccbdd  25782  ovolicc2lem4  25841  0pledm  25994  cniccibl  26161  cnicciblnc  26163  c1lip1  26317  lhop1  26334  itgsubstlem  26368  ulmshftlem  26716  ulm0  26718  ulmcau  26722  rlimcnp  27293  fsumdvdsmul  27522  chtub  27539  2sqlem10  27755  dchrisum0flb  27837  pntpbnd1  27913  pntpbnd  27915  pntibndlem2  27918  pntibndlem3  27919  pntibnd  27920  pntlemi  27931  pntleme  27935  pntlem3  27936  pntlemp  27937  pntleml  27938  pnt3  27939  madebdaylemlrcut  28285  noinds  28331  no2indlesm  28340  no3inds  28344  precsexlem9  28601  istrkgld  28921  trgcgrg  28978  tgcgr4  28994  isperp  29187  brbtwn  29477  usgruspgrb  29764  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  nbgr1vtx  29939  uvtx01vtx  29978  cplgr1v  30011  wlkeq  30214  wlkl1loop  30218  uspgr2wlkeq  30226  upgr2wlk  30247  redwlk  30251  wlkp1lem8  30259  usgr2wlkneq  30342  usgr2trlncl  30346  usgr2pthlem  30349  usgr2pth  30350  pthdlem1  30352  uspgrn2crct  30397  crctcshwlkn0  30410  wwlknp  30432  wwlksn0s  30450  wlkiswwlks1  30456  wlkiswwlks2lem4  30461  wwlksnred  30481  rusgrnumwwlkl1  30560  clwwlkccatlem  30580  clwlkclwwlklem2a1  30583  clwlkclwwlklem2a  30589  clwlkclwwlklem3  30592  clwwlkn  30617  clwwlknp  30628  clwwlkinwwlk  30631  clwwlkn1  30632  clwwlkn2  30635  clwwlkel  30637  clwwlkf  30638  clwwlkwwlksb  30645  1ewlk  30706  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  dfconngr1  30789  isconngr1  30791  frgr3v  30876  frgrwopregasn  30917  frgrwopregbsn  30918  ubth  31475  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1  33257  fnpreimac  33264  fxpgaval  33728  crngmxidl  33994  lmxrge0  34584  measval  34831  isrnmeas  34833  sitgval  34964  eulerpartlemo  34997  eulerpartlemn  35013  onvf1odlem4  35885  subfacp1lem3  35947  subfacp1lem5  35949  txpconn  35997  cvxpconn  36007  cvmscbv  36023  cvmsi  36030  cvmsval  36031  satf  36118  sat1el2xp  36144  elmrsubrn  36285  weiunlem  37251  bj-raldifsn  38021  poimirlem26  38565  poimirlem27  38566  poimirlem31  38570  poimirlem32  38571  heicant  38574  mblfinlem3  38578  ovoliunnfl  38581  voliunnfl  38583  volsupnfl  38584  sdclem1  38678  fdc  38680  rrncmslem  38767  isass  38781  isrngod  38833  isgrpda  38890  iscom2  38930  pautsetN  41156  tendofset  41816  tendoset  41817  hdmap14lem13  42938  3factsumint1  43072  sticksstones3  43199  kelac1  44065  gicabl  44101  cantnfresb  44326  safesnsupfilb  44419  fiinfi  44574  clsk1independent  45046  wessf1ornlem  46200  uzub  46441  rexanuz2nf  46502  mccl  46610  climsuse  46620  limsupmnfuzlem  46736  limsupmnfuz  46737  limsupre3uzlem  46745  limsupre3uz  46746  limsupreuz  46747  0cnv  46752  climuz  46754  lmbr3  46757  limsupgt  46788  liminflt  46815  xlimpnfxnegmnf  46824  xlimmnf  46851  xlimpnf  46852  xlimmnfmpt  46853  xlimpnfmpt  46854  dfxlim2  46858  fourierdlem2  47119  fourierdlem3  47120  fourierdlem31  47148  fourierdlem47  47163  fourierdlem70  47186  fourierdlem71  47187  fourierdlem80  47196  fourierdlem103  47219  fourierdlem104  47220  fourierdlem113  47229  etransclem48  47292  etransc  47293  caragenval  47503  omessle  47508  smfmullem2  47802  smfmul  47805  2ffzoeq  48398  iccpval  48497  iccpartigtl  48505  nprmmul1  48609  cycl3grtrilem  49044  grlimedgclnbgr  49093  grlimgrtri  49101  grilcbri2  49109  usgrexmpl2trifr  49135  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  lindsrng01  49580  rrx2line  49852  initopropd  50351  termopropd  50352  fucofulem2  50419  thincpropd  50550  isinito2lem  50606