Theorem raleqdv 3295

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-ral 3051  df-rex 3060

This theorem is referenced by:  raleqtrdv  3297  raleqtrrdv  3299  raleqbidva  3301  raleleqOLD  3312  raldifeq  4445  frpoinsg  6300  f12dfv  7219  f13dfv  7220  cbvfo  7235  isoselem  7287  ofrfvalg  7630  omsinds  7829  frpoins3xpg  8082  frpoins3xp3g  8083  frrlem4  8231  issmo2  8281  smoeq  8282  on2ind  8597  on3ind  8598  naddsuc2  8629  frfi  9187  marypha1lem  9338  marypha1  9339  dfoi  9418  oieq2  9420  ordtypecbv  9424  ordtypelem2  9426  ordtypelem3  9427  ordtypelem9  9433  wemapwe  9608  ttrclss  9631  ttrclselem2  9637  frinsg  9665  tcrank  9798  isacn  9956  pwsdompw  10115  isfin2  10206  isfin3ds  10241  isf33lem  10278  hsmexlem4  10341  zorn2lem6  10413  zorn2lem7  10414  zorn2g  10415  fpwwe2lem12  10555  uzsupss  12855  fzrevral2  13531  fzrevral3  13532  fzshftral  13533  fzoshftral  13705  uzsinds  13912  expmulnbnd  14160  eqs1  14538  swrdspsleq  14591  pfxeq  14621  pfxsuffeqwrdeq  14623  repswsymballbi  14705  cshw1  14747  pfx2  14872  wwlktovf1  14882  eqwrds3  14886  rexuz3  15274  rexuzre  15278  limsupgle  15402  rlim  15420  climconst  15468  rlimclim1  15470  climshftlem  15499  isercoll  15593  caucvgb  15605  serf0  15606  mertenslem1  15809  coprmprod  16590  coprmproddvds  16592  prmind2  16614  vdwlem10  16920  vdwlem13  16923  vdwnnlem2  16926  vdwnnlem3  16927  vdwnn  16928  ramval  16938  ramz  16955  prmgaplem5  16985  isacs  17576  cidpropd  17635  monpropd  17663  isssc  17746  fullsubc  17776  funcpropd  17828  isfth  17842  fthpropd  17849  grpidpropd  18589  sgrppropd  18658  mndpropd  18686  nmznsg  19099  ghmnsgima  19171  symgextfo  19353  gsmsymgrfixlem1  19358  gsmsymgrfix  19359  fvcosymgeq  19360  gsmsymgreqlem2  19362  psgnunilem3  19427  sylow2blem3  19553  sylow3lem6  19563  cmnpropd  19722  telgsumfzs  19920  rngpropd  20111  ringpropd  20225  c0snmgmhm  20400  abvpropd  20770  lsspropd  20971  lmhmpropd  21027  lbspropd  21053  pj1lmhm  21054  psgndiflemB  21557  phlpropd  21612  islindf  21769  lindfmm  21784  islindf4  21795  islindf5  21796  assapropd  21829  scmatf1  22477  isclo  23033  lmfval  23178  lmconst  23207  iscnrm2  23284  ist0-2  23290  ist1-2  23293  ishaus2  23297  subislly  23427  elpt  23518  elptr  23519  ptbasfi  23527  fclscmp  23976  ufilcmp  23978  cnpfcf  23987  alexsubALTlem1  23993  alexsubALTlem2  23994  alexsubALTlem4  23996  tmdgsum2  24042  tsmsf1o  24091  ustval  24149  ucnval  24222  imasdsf1olem  24319  imasf1oxmet  24321  imasf1omet  24322  metss  24454  prdsxmslem2  24475  lebnumlem3  24920  ishtpy  24929  lmnn  25221  evthicc  25418  cniccbdd  25420  ovolicc2lem4  25479  0pledm  25632  cniccibl  25800  cnicciblnc  25802  c1lip1  25960  lhop1  25977  itgsubstlem  26013  ulmshftlem  26356  ulm0  26358  ulmcau  26362  rlimcnp  26933  fsumdvdsmul  27163  fsumdvdsmulOLD  27165  chtub  27181  2sqlem10  27397  dchrisum0flb  27479  pntpbnd1  27555  pntpbnd  27557  pntibndlem2  27560  pntibndlem3  27561  pntibnd  27562  pntlemi  27573  pntleme  27577  pntlem3  27578  pntlemp  27579  pntleml  27580  pnt3  27581  madebdaylemlrcut  27879  noinds  27925  no2indslem  27934  no3inds  27938  precsexlem9  28194  istrkgld  28512  trgcgrg  28568  tgcgr4  28584  isperp  28765  brbtwn  28953  usgruspgrb  29237  nbgr2vtx1edg  29404  nbuhgr2vtx1edgb  29406  nbgr1vtx  29412  uvtx01vtx  29451  cplgr1v  29484  wlkeq  29688  wlkl1loop  29692  uspgr2wlkeq  29700  upgr2wlk  29721  redwlk  29725  wlkp1lem8  29733  usgr2wlkneq  29810  usgr2trlncl  29814  usgr2pthlem  29817  usgr2pth  29818  pthdlem1  29820  uspgrn2crct  29862  crctcshwlkn0  29875  wwlknp  29897  wwlksn0s  29915  wlkiswwlks1  29921  wlkiswwlks2lem4  29926  wwlksnred  29946  rusgrnumwwlkl1  30025  clwwlkccatlem  30045  clwlkclwwlklem2a1  30048  clwlkclwwlklem2a  30054  clwlkclwwlklem3  30057  clwwlkn  30082  clwwlknp  30093  clwwlkinwwlk  30096  clwwlkn1  30097  clwwlkn2  30100  clwwlkel  30102  clwwlkf  30103  clwwlkwwlksb  30110  1ewlk  30171  upgr3v3e3cycl  30236  upgr4cycl4dv4e  30241  dfconngr1  30244  isconngr1  30246  frgr3v  30331  frgrwopregasn  30372  frgrwopregbsn  30373  ubth  30929  acunirnmpt2  32718  acunirnmpt2f  32719  aciunf1  32721  fnpreimac  32728  fxpgaval  33228  crngmxidl  33529  lmxrge0  34088  measval  34334  isrnmeas  34336  sitgval  34468  eulerpartlemo  34501  eulerpartlemn  34517  onvf1odlem4  35279  subfacp1lem3  35355  subfacp1lem5  35357  txpconn  35405  cvxpconn  35415  cvmscbv  35431  cvmsi  35438  cvmsval  35439  satf  35526  sat1el2xp  35552  elmrsubrn  35693  weiunlem2  36636  bj-raldifsn  37274  poimirlem26  37816  poimirlem27  37817  poimirlem31  37821  poimirlem32  37822  heicant  37825  mblfinlem3  37829  ovoliunnfl  37832  voliunnfl  37834  volsupnfl  37835  sdclem1  37913  fdc  37915  rrncmslem  38002  isass  38016  isrngod  38068  isgrpda  38125  iscom2  38165  pautsetN  40393  tendofset  41053  tendoset  41054  hdmap14lem13  42175  3factsumint1  42310  sticksstones3  42437  kelac1  43342  gicabl  43378  cantnfresb  43603  safesnsupfilb  43696  fiinfi  43851  clsk1independent  44324  scotteqd  44515  wessf1ornlem  45466  uzub  45712  rexanuz2nf  45773  mccl  45881  climsuse  45891  limsupmnfuzlem  46007  limsupmnfuz  46008  limsupre3uzlem  46016  limsupre3uz  46017  limsupreuz  46018  0cnv  46023  climuz  46025  lmbr3  46028  limsupgt  46059  liminflt  46086  xlimpnfxnegmnf  46095  xlimmnf  46122  xlimpnf  46123  xlimmnfmpt  46124  xlimpnfmpt  46125  dfxlim2  46129  fourierdlem2  46390  fourierdlem3  46391  fourierdlem31  46419  fourierdlem47  46434  fourierdlem70  46457  fourierdlem71  46458  fourierdlem80  46467  fourierdlem103  46490  fourierdlem104  46491  fourierdlem113  46500  etransclem48  46563  etransc  46564  caragenval  46774  omessle  46779  smfmullem2  47073  smfmul  47076  2ffzoeq  47610  iccpval  47698  iccpartigtl  47706  cycl3grtrilem  48229  grlimedgclnbgr  48278  grlimgrtri  48286  grilcbri2  48294  usgrexmpl2trifr  48320  gpg5nbgrvtx03star  48363  gpg5nbgr3star  48364  lindsrng01  48751  rrx2line  49023  initopropd  49525  termopropd  49526  fucofulem2  49593  thincpropd  49724  isinito2lem  49780