Theorem raleqdv 3294

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ral 3050  df-rex 3059

This theorem is referenced by:  raleqtrdv  3296  raleqtrrdv  3298  raleqbidva  3300  raleleqOLD  3311  raldifeq  4445  frpoinsg  6298  f12dfv  7216  f13dfv  7217  cbvfo  7232  isoselem  7284  ofrfvalg  7627  omsinds  7826  frpoins3xpg  8079  frpoins3xp3g  8080  frrlem4  8228  issmo2  8278  smoeq  8279  on2ind  8593  on3ind  8594  naddsuc2  8625  frfi  9179  marypha1lem  9327  marypha1  9328  dfoi  9407  oieq2  9409  ordtypecbv  9413  ordtypelem2  9415  ordtypelem3  9416  ordtypelem9  9422  wemapwe  9597  ttrclss  9620  ttrclselem2  9626  frinsg  9654  tcrank  9787  isacn  9945  pwsdompw  10104  isfin2  10195  isfin3ds  10230  isf33lem  10267  hsmexlem4  10330  zorn2lem6  10402  zorn2lem7  10403  zorn2g  10404  fpwwe2lem12  10543  uzsupss  12848  fzrevral2  13523  fzrevral3  13524  fzshftral  13525  fzoshftral  13697  uzsinds  13904  expmulnbnd  14152  eqs1  14530  swrdspsleq  14583  pfxeq  14613  pfxsuffeqwrdeq  14615  repswsymballbi  14697  cshw1  14739  pfx2  14864  wwlktovf1  14874  eqwrds3  14878  rexuz3  15266  rexuzre  15270  limsupgle  15394  rlim  15412  climconst  15460  rlimclim1  15462  climshftlem  15491  isercoll  15585  caucvgb  15597  serf0  15598  mertenslem1  15801  coprmprod  16582  coprmproddvds  16584  prmind2  16606  vdwlem10  16912  vdwlem13  16915  vdwnnlem2  16918  vdwnnlem3  16919  vdwnn  16920  ramval  16930  ramz  16947  prmgaplem5  16977  isacs  17567  cidpropd  17626  monpropd  17654  isssc  17737  fullsubc  17767  funcpropd  17819  isfth  17833  fthpropd  17840  grpidpropd  18580  sgrppropd  18649  mndpropd  18677  nmznsg  19090  ghmnsgima  19162  symgextfo  19344  gsmsymgrfixlem1  19349  gsmsymgrfix  19350  fvcosymgeq  19351  gsmsymgreqlem2  19353  psgnunilem3  19418  sylow2blem3  19544  sylow3lem6  19554  cmnpropd  19713  telgsumfzs  19911  rngpropd  20102  ringpropd  20216  c0snmgmhm  20390  abvpropd  20760  lsspropd  20961  lmhmpropd  21017  lbspropd  21043  pj1lmhm  21044  psgndiflemB  21547  phlpropd  21602  islindf  21759  lindfmm  21774  islindf4  21785  islindf5  21786  assapropd  21819  scmatf1  22456  isclo  23012  lmfval  23157  lmconst  23186  iscnrm2  23263  ist0-2  23269  ist1-2  23272  ishaus2  23276  subislly  23406  elpt  23497  elptr  23498  ptbasfi  23506  fclscmp  23955  ufilcmp  23957  cnpfcf  23966  alexsubALTlem1  23972  alexsubALTlem2  23973  alexsubALTlem4  23975  tmdgsum2  24021  tsmsf1o  24070  ustval  24128  ucnval  24201  imasdsf1olem  24298  imasf1oxmet  24300  imasf1omet  24301  metss  24433  prdsxmslem2  24454  lebnumlem3  24899  ishtpy  24908  lmnn  25200  evthicc  25397  cniccbdd  25399  ovolicc2lem4  25458  0pledm  25611  cniccibl  25779  cnicciblnc  25781  c1lip1  25939  lhop1  25956  itgsubstlem  25992  ulmshftlem  26335  ulm0  26337  ulmcau  26341  rlimcnp  26912  fsumdvdsmul  27142  fsumdvdsmulOLD  27144  chtub  27160  2sqlem10  27376  dchrisum0flb  27458  pntpbnd1  27534  pntpbnd  27536  pntibndlem2  27539  pntibndlem3  27540  pntibnd  27541  pntlemi  27552  pntleme  27556  pntlem3  27557  pntlemp  27558  pntleml  27559  pnt3  27560  madebdaylemlrcut  27854  noinds  27898  no2indslem  27907  no3inds  27911  precsexlem9  28163  istrkgld  28447  trgcgrg  28503  tgcgr4  28519  isperp  28700  brbtwn  28888  usgruspgrb  29172  nbgr2vtx1edg  29339  nbuhgr2vtx1edgb  29341  nbgr1vtx  29347  uvtx01vtx  29386  cplgr1v  29419  wlkeq  29623  wlkl1loop  29627  uspgr2wlkeq  29635  upgr2wlk  29656  redwlk  29660  wlkp1lem8  29668  usgr2wlkneq  29745  usgr2trlncl  29749  usgr2pthlem  29752  usgr2pth  29753  pthdlem1  29755  uspgrn2crct  29797  crctcshwlkn0  29810  wwlknp  29832  wwlksn0s  29850  wlkiswwlks1  29856  wlkiswwlks2lem4  29861  wwlksnred  29881  rusgrnumwwlkl1  29960  clwwlkccatlem  29980  clwlkclwwlklem2a1  29983  clwlkclwwlklem2a  29989  clwlkclwwlklem3  29992  clwwlkn  30017  clwwlknp  30028  clwwlkinwwlk  30031  clwwlkn1  30032  clwwlkn2  30035  clwwlkel  30037  clwwlkf  30038  clwwlkwwlksb  30045  1ewlk  30106  upgr3v3e3cycl  30171  upgr4cycl4dv4e  30176  dfconngr1  30179  isconngr1  30181  frgr3v  30266  frgrwopregasn  30307  frgrwopregbsn  30308  ubth  30864  acunirnmpt2  32653  acunirnmpt2f  32654  aciunf1  32656  fnpreimac  32664  fxpgaval  33147  crngmxidl  33445  lmxrge0  33976  measval  34222  isrnmeas  34224  sitgval  34356  eulerpartlemo  34389  eulerpartlemn  34405  onvf1odlem4  35161  subfacp1lem3  35237  subfacp1lem5  35239  txpconn  35287  cvxpconn  35297  cvmscbv  35313  cvmsi  35320  cvmsval  35321  satf  35408  sat1el2xp  35434  elmrsubrn  35575  weiunlem2  36518  bj-raldifsn  37155  poimirlem26  37696  poimirlem27  37697  poimirlem31  37701  poimirlem32  37702  heicant  37705  mblfinlem3  37709  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  sdclem1  37793  fdc  37795  rrncmslem  37882  isass  37896  isrngod  37948  isgrpda  38005  iscom2  38045  pautsetN  40207  tendofset  40867  tendoset  40868  hdmap14lem13  41989  3factsumint1  42124  sticksstones3  42251  kelac1  43170  gicabl  43206  cantnfresb  43431  safesnsupfilb  43525  fiinfi  43680  clsk1independent  44153  scotteqd  44344  wessf1ornlem  45296  uzub  45543  rexanuz2nf  45604  mccl  45712  climsuse  45722  limsupmnfuzlem  45838  limsupmnfuz  45839  limsupre3uzlem  45847  limsupre3uz  45848  limsupreuz  45849  0cnv  45854  climuz  45856  lmbr3  45859  limsupgt  45890  liminflt  45917  xlimpnfxnegmnf  45926  xlimmnf  45953  xlimpnf  45954  xlimmnfmpt  45955  xlimpnfmpt  45956  dfxlim2  45960  fourierdlem2  46221  fourierdlem3  46222  fourierdlem31  46250  fourierdlem47  46265  fourierdlem70  46288  fourierdlem71  46289  fourierdlem80  46298  fourierdlem103  46321  fourierdlem104  46322  fourierdlem113  46331  etransclem48  46394  etransc  46395  caragenval  46605  omessle  46610  smfmullem2  46904  smfmul  46907  2ffzoeq  47441  iccpval  47529  iccpartigtl  47537  cycl3grtrilem  48060  grlimedgclnbgr  48109  grlimgrtri  48117  grilcbri2  48125  usgrexmpl2trifr  48151  gpg5nbgrvtx03star  48194  gpg5nbgr3star  48195  lindsrng01  48583  rrx2line  48855  initopropd  49358  termopropd  49359  fucofulem2  49426  thincpropd  49557  isinito2lem  49613