Theorem raleqdv 3296

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 3293	. 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  3298  raleqtrrdv  3300  raleqbidva  3302  raleleqOLD  3313  raldifeq  4453  frpoinsg  6304  f12dfv  7230  f13dfv  7231  cbvfo  7246  isoselem  7298  ofrfvalg  7641  omsinds  7843  frpoins3xpg  8096  frpoins3xp3g  8097  frrlem4  8245  issmo2  8295  smoeq  8296  on2ind  8610  on3ind  8611  naddsuc2  8642  frfi  9208  marypha1lem  9360  marypha1  9361  dfoi  9440  oieq2  9442  ordtypecbv  9446  ordtypelem2  9448  ordtypelem3  9449  ordtypelem9  9455  wemapwe  9626  ttrclss  9649  ttrclselem2  9655  frinsg  9680  tcrank  9813  isacn  9973  pwsdompw  10132  isfin2  10223  isfin3ds  10258  isf33lem  10295  hsmexlem4  10358  zorn2lem6  10430  zorn2lem7  10431  zorn2g  10432  fpwwe2lem12  10571  uzsupss  12875  fzrevral2  13550  fzrevral3  13551  fzshftral  13552  fzoshftral  13721  uzsinds  13928  expmulnbnd  14176  eqs1  14553  swrdspsleq  14606  pfxeq  14637  pfxsuffeqwrdeq  14639  repswsymballbi  14721  cshw1  14763  pfx2  14889  wwlktovf1  14899  eqwrds3  14903  rexuz3  15291  rexuzre  15295  limsupgle  15419  rlim  15437  climconst  15485  rlimclim1  15487  climshftlem  15516  isercoll  15610  caucvgb  15622  serf0  15623  mertenslem1  15826  coprmprod  16607  coprmproddvds  16609  prmind2  16631  vdwlem10  16937  vdwlem13  16940  vdwnnlem2  16943  vdwnnlem3  16944  vdwnn  16945  ramval  16955  ramz  16972  prmgaplem5  17002  isacs  17592  cidpropd  17651  monpropd  17679  isssc  17762  fullsubc  17792  funcpropd  17844  isfth  17858  fthpropd  17865  grpidpropd  18571  sgrppropd  18640  mndpropd  18668  nmznsg  19082  ghmnsgima  19154  symgextfo  19336  gsmsymgrfixlem1  19341  gsmsymgrfix  19342  fvcosymgeq  19343  gsmsymgreqlem2  19345  psgnunilem3  19410  sylow2blem3  19536  sylow3lem6  19546  cmnpropd  19705  telgsumfzs  19903  rngpropd  20094  ringpropd  20208  c0snmgmhm  20382  abvpropd  20755  lsspropd  20956  lmhmpropd  21012  lbspropd  21038  pj1lmhm  21039  psgndiflemB  21542  phlpropd  21597  islindf  21754  lindfmm  21769  islindf4  21780  islindf5  21781  assapropd  21814  scmatf1  22451  isclo  23007  lmfval  23152  lmconst  23181  iscnrm2  23258  ist0-2  23264  ist1-2  23267  ishaus2  23271  subislly  23401  elpt  23492  elptr  23493  ptbasfi  23501  fclscmp  23950  ufilcmp  23952  cnpfcf  23961  alexsubALTlem1  23967  alexsubALTlem2  23968  alexsubALTlem4  23970  tmdgsum2  24016  tsmsf1o  24065  ustval  24123  ucnval  24197  imasdsf1olem  24294  imasf1oxmet  24296  imasf1omet  24297  metss  24429  prdsxmslem2  24450  lebnumlem3  24895  ishtpy  24904  lmnn  25196  evthicc  25393  cniccbdd  25395  ovolicc2lem4  25454  0pledm  25607  cniccibl  25775  cnicciblnc  25777  c1lip1  25935  lhop1  25952  itgsubstlem  25988  ulmshftlem  26331  ulm0  26333  ulmcau  26337  rlimcnp  26908  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  chtub  27156  2sqlem10  27372  dchrisum0flb  27454  pntpbnd1  27530  pntpbnd  27532  pntibndlem2  27535  pntibndlem3  27536  pntibnd  27537  pntlemi  27548  pntleme  27552  pntlem3  27553  pntlemp  27554  pntleml  27555  pnt3  27556  madebdaylemlrcut  27848  noinds  27892  no2indslem  27901  no3inds  27905  precsexlem9  28157  istrkgld  28439  trgcgrg  28495  tgcgr4  28511  isperp  28692  brbtwn  28879  usgruspgrb  29163  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  nbgr1vtx  29338  uvtx01vtx  29377  cplgr1v  29410  wlkeq  29614  wlkl1loop  29618  uspgr2wlkeq  29626  upgr2wlk  29647  redwlk  29651  wlkp1lem8  29659  usgr2wlkneq  29736  usgr2trlncl  29740  usgr2pthlem  29743  usgr2pth  29744  pthdlem1  29746  uspgrn2crct  29788  crctcshwlkn0  29801  wwlknp  29823  wwlksn0s  29841  wlkiswwlks1  29847  wlkiswwlks2lem4  29852  wwlksnred  29872  rusgrnumwwlkl1  29948  clwwlkccatlem  29968  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a  29977  clwlkclwwlklem3  29980  clwwlkn  30005  clwwlknp  30016  clwwlkinwwlk  30019  clwwlkn1  30020  clwwlkn2  30023  clwwlkel  30025  clwwlkf  30026  clwwlkwwlksb  30033  1ewlk  30094  upgr3v3e3cycl  30159  upgr4cycl4dv4e  30164  dfconngr1  30167  isconngr1  30169  frgr3v  30254  frgrwopregasn  30295  frgrwopregbsn  30296  ubth  30852  acunirnmpt2  32634  acunirnmpt2f  32635  aciunf1  32637  fnpreimac  32645  fxpgaval  33139  crngmxidl  33433  lmxrge0  33935  measval  34181  isrnmeas  34183  sitgval  34316  eulerpartlemo  34349  eulerpartlemn  34365  onvf1odlem4  35086  subfacp1lem3  35162  subfacp1lem5  35164  txpconn  35212  cvxpconn  35222  cvmscbv  35238  cvmsi  35245  cvmsval  35246  satf  35333  sat1el2xp  35359  elmrsubrn  35500  weiunlem2  36444  bj-raldifsn  37081  poimirlem26  37633  poimirlem27  37634  poimirlem31  37638  poimirlem32  37639  heicant  37642  mblfinlem3  37646  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  sdclem1  37730  fdc  37732  rrncmslem  37819  isass  37833  isrngod  37885  isgrpda  37942  iscom2  37982  pautsetN  40085  tendofset  40745  tendoset  40746  hdmap14lem13  41867  3factsumint1  42002  sticksstones3  42129  kelac1  43045  gicabl  43081  cantnfresb  43306  safesnsupfilb  43400  fiinfi  43555  clsk1independent  44028  scotteqd  44219  wessf1ornlem  45172  uzub  45420  rexanuz2nf  45481  mccl  45589  climsuse  45599  limsupmnfuzlem  45717  limsupmnfuz  45718  limsupre3uzlem  45726  limsupre3uz  45727  limsupreuz  45728  0cnv  45733  climuz  45735  lmbr3  45738  limsupgt  45769  liminflt  45796  xlimpnfxnegmnf  45805  xlimmnf  45832  xlimpnf  45833  xlimmnfmpt  45834  xlimpnfmpt  45835  dfxlim2  45839  fourierdlem2  46100  fourierdlem3  46101  fourierdlem31  46129  fourierdlem47  46144  fourierdlem70  46167  fourierdlem71  46168  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  fourierdlem113  46210  etransclem48  46273  etransc  46274  caragenval  46484  omessle  46489  smfmullem2  46783  smfmul  46786  2ffzoeq  47321  iccpval  47409  iccpartigtl  47417  cycl3grtrilem  47938  grlimgrtri  47988  grilcbri2  47996  usgrexmpl2trifr  48021  gpg5nbgrvtx03star  48064  gpg5nbgr3star  48065  lindsrng01  48450  rrx2line  48722  initopropd  49225  termopropd  49226  fucofulem2  49293  thincpropd  49424  isinito2lem  49480