Theorem raleqdv 3298

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3063

This theorem is referenced by:  raleqtrdv  3300  raleqtrrdv  3302  raleqbidva  3304  raleleqOLD  3315  raldifeq  4448  frpoinsg  6311  f12dfv  7231  f13dfv  7232  cbvfo  7247  isoselem  7299  ofrfvalg  7642  omsinds  7841  frpoins3xpg  8094  frpoins3xp3g  8095  frrlem4  8243  issmo2  8293  smoeq  8294  on2ind  8609  on3ind  8610  naddsuc2  8641  frfi  9199  marypha1lem  9350  marypha1  9351  dfoi  9430  oieq2  9432  ordtypecbv  9436  ordtypelem2  9438  ordtypelem3  9439  ordtypelem9  9445  wemapwe  9620  ttrclss  9643  ttrclselem2  9649  frinsg  9677  tcrank  9810  isacn  9968  pwsdompw  10127  isfin2  10218  isfin3ds  10253  isf33lem  10290  hsmexlem4  10353  zorn2lem6  10425  zorn2lem7  10426  zorn2g  10427  fpwwe2lem12  10567  uzsupss  12867  fzrevral2  13543  fzrevral3  13544  fzshftral  13545  fzoshftral  13717  uzsinds  13924  expmulnbnd  14172  eqs1  14550  swrdspsleq  14603  pfxeq  14633  pfxsuffeqwrdeq  14635  repswsymballbi  14717  cshw1  14759  pfx2  14884  wwlktovf1  14894  eqwrds3  14898  rexuz3  15286  rexuzre  15290  limsupgle  15414  rlim  15432  climconst  15480  rlimclim1  15482  climshftlem  15511  isercoll  15605  caucvgb  15617  serf0  15618  mertenslem1  15821  coprmprod  16602  coprmproddvds  16604  prmind2  16626  vdwlem10  16932  vdwlem13  16935  vdwnnlem2  16938  vdwnnlem3  16939  vdwnn  16940  ramval  16950  ramz  16967  prmgaplem5  16997  isacs  17588  cidpropd  17647  monpropd  17675  isssc  17758  fullsubc  17788  funcpropd  17840  isfth  17854  fthpropd  17861  grpidpropd  18601  sgrppropd  18670  mndpropd  18698  nmznsg  19114  ghmnsgima  19186  symgextfo  19368  gsmsymgrfixlem1  19373  gsmsymgrfix  19374  fvcosymgeq  19375  gsmsymgreqlem2  19377  psgnunilem3  19442  sylow2blem3  19568  sylow3lem6  19578  cmnpropd  19737  telgsumfzs  19935  rngpropd  20126  ringpropd  20240  c0snmgmhm  20415  abvpropd  20785  lsspropd  20986  lmhmpropd  21042  lbspropd  21068  pj1lmhm  21069  psgndiflemB  21572  phlpropd  21627  islindf  21784  lindfmm  21799  islindf4  21810  islindf5  21811  assapropd  21844  scmatf1  22492  isclo  23048  lmfval  23193  lmconst  23222  iscnrm2  23299  ist0-2  23305  ist1-2  23308  ishaus2  23312  subislly  23442  elpt  23533  elptr  23534  ptbasfi  23542  fclscmp  23991  ufilcmp  23993  cnpfcf  24002  alexsubALTlem1  24008  alexsubALTlem2  24009  alexsubALTlem4  24011  tmdgsum2  24057  tsmsf1o  24106  ustval  24164  ucnval  24237  imasdsf1olem  24334  imasf1oxmet  24336  imasf1omet  24337  metss  24469  prdsxmslem2  24490  lebnumlem3  24935  ishtpy  24944  lmnn  25236  evthicc  25433  cniccbdd  25435  ovolicc2lem4  25494  0pledm  25647  cniccibl  25815  cnicciblnc  25817  c1lip1  25975  lhop1  25992  itgsubstlem  26028  ulmshftlem  26371  ulm0  26373  ulmcau  26377  rlimcnp  26948  fsumdvdsmul  27178  fsumdvdsmulOLD  27180  chtub  27196  2sqlem10  27412  dchrisum0flb  27494  pntpbnd1  27570  pntpbnd  27572  pntibndlem2  27575  pntibndlem3  27576  pntibnd  27577  pntlemi  27588  pntleme  27592  pntlem3  27593  pntlemp  27594  pntleml  27595  pnt3  27596  madebdaylemlrcut  27912  noinds  27958  no2indlesm  27967  no3inds  27971  precsexlem9  28228  istrkgld  28548  trgcgrg  28605  tgcgr4  28621  isperp  28802  brbtwn  28990  usgruspgrb  29274  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  nbgr1vtx  29449  uvtx01vtx  29488  cplgr1v  29521  wlkeq  29725  wlkl1loop  29729  uspgr2wlkeq  29737  upgr2wlk  29758  redwlk  29762  wlkp1lem8  29770  usgr2wlkneq  29847  usgr2trlncl  29851  usgr2pthlem  29854  usgr2pth  29855  pthdlem1  29857  uspgrn2crct  29899  crctcshwlkn0  29912  wwlknp  29934  wwlksn0s  29952  wlkiswwlks1  29958  wlkiswwlks2lem4  29963  wwlksnred  29983  rusgrnumwwlkl1  30062  clwwlkccatlem  30082  clwlkclwwlklem2a1  30085  clwlkclwwlklem2a  30091  clwlkclwwlklem3  30094  clwwlkn  30119  clwwlknp  30130  clwwlkinwwlk  30133  clwwlkn1  30134  clwwlkn2  30137  clwwlkel  30139  clwwlkf  30140  clwwlkwwlksb  30147  1ewlk  30208  upgr3v3e3cycl  30273  upgr4cycl4dv4e  30278  dfconngr1  30281  isconngr1  30283  frgr3v  30368  frgrwopregasn  30409  frgrwopregbsn  30410  ubth  30967  acunirnmpt2  32756  acunirnmpt2f  32757  aciunf1  32759  fnpreimac  32766  fxpgaval  33267  crngmxidl  33568  lmxrge0  34136  measval  34382  isrnmeas  34384  sitgval  34516  eulerpartlemo  34549  eulerpartlemn  34565  onvf1odlem4  35328  subfacp1lem3  35404  subfacp1lem5  35406  txpconn  35454  cvxpconn  35464  cvmscbv  35480  cvmsi  35487  cvmsval  35488  satf  35575  sat1el2xp  35601  elmrsubrn  35742  weiunlem  36685  bj-raldifsn  37380  poimirlem26  37926  poimirlem27  37927  poimirlem31  37931  poimirlem32  37932  heicant  37935  mblfinlem3  37939  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  sdclem1  38023  fdc  38025  rrncmslem  38112  isass  38126  isrngod  38178  isgrpda  38235  iscom2  38275  pautsetN  40503  tendofset  41163  tendoset  41164  hdmap14lem13  42285  3factsumint1  42420  sticksstones3  42547  kelac1  43449  gicabl  43485  cantnfresb  43710  safesnsupfilb  43803  fiinfi  43958  clsk1independent  44431  scotteqd  44622  wessf1ornlem  45573  uzub  45818  rexanuz2nf  45879  mccl  45987  climsuse  45997  limsupmnfuzlem  46113  limsupmnfuz  46114  limsupre3uzlem  46122  limsupre3uz  46123  limsupreuz  46124  0cnv  46129  climuz  46131  lmbr3  46134  limsupgt  46165  liminflt  46192  xlimpnfxnegmnf  46201  xlimmnf  46228  xlimpnf  46229  xlimmnfmpt  46230  xlimpnfmpt  46231  dfxlim2  46235  fourierdlem2  46496  fourierdlem3  46497  fourierdlem31  46525  fourierdlem47  46540  fourierdlem70  46563  fourierdlem71  46564  fourierdlem80  46573  fourierdlem103  46596  fourierdlem104  46597  fourierdlem113  46606  etransclem48  46669  etransc  46670  caragenval  46880  omessle  46885  smfmullem2  47179  smfmul  47182  2ffzoeq  47716  iccpval  47804  iccpartigtl  47812  cycl3grtrilem  48335  grlimedgclnbgr  48384  grlimgrtri  48392  grilcbri2  48400  usgrexmpl2trifr  48426  gpg5nbgrvtx03star  48469  gpg5nbgr3star  48470  lindsrng01  48857  rrx2line  49129  initopropd  49631  termopropd  49632  fucofulem2  49699  thincpropd  49830  isinito2lem  49886