Theorem raleqdv 3322

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ral 3079  df-rex 3089

This theorem is used by:  raleqtrdv  3324  raleqtrrdv  3326  raleqbidva  3328  raldifeq  4453  frpoinsg  6344  f12dfv  7271  f13dfv  7272  cbvfo  7287  isoselem  7339  ofrfvalg  7684  omsinds  7881  frpoins3xpg  8134  frpoins3xp3g  8135  frrlem4  8284  issmo2  8334  smoeq  8335  on2ind  8653  on3ind  8654  naddsuc2  8686  frfi  9243  marypha1lem  9391  marypha1  9392  dfoi  9471  oieq2  9473  ordtypecbv  9477  ordtypelem2  9479  ordtypelem3  9480  ordtypelem9  9486  wemapwe  9664  ttrclss  9687  ttrclselem2  9693  frinsg  9721  tcrank  9854  scotteqd  9857  isacn  10035  pwsdompw  10193  isfin2  10284  isfin3ds  10319  isf33lem  10356  hsmexlem4  10419  zorn2lem6  10491  zorn2lem7  10492  zorn2g  10493  fpwwe2lem12  10633  uzsupss  12970  fzrevral2  13648  fzrevral3  13649  fzshftral  13650  fzoshftral  13823  uzsinds  14030  expmulnbnd  14278  eqs1  14657  swrdspsleq  14710  pfxeq  14740  pfxsuffeqwrdeq  14742  repswsymballbi  14824  cshw1  14866  pfx2  14991  wwlktovf1  15001  eqwrds3  15005  rexuz3  15407  rexuzre  15411  limsupgle  15535  rlim  15553  climconst  15601  rlimclim1  15603  climshftlem  15632  isercoll  15726  caucvgb  15738  serf0  15739  mertenslem1  15945  coprmprod  16725  coprmproddvds  16727  prmind2  16749  vdwlem10  17056  vdwlem13  17059  vdwnnlem2  17062  vdwnnlem3  17063  vdwnn  17064  ramval  17074  ramz  17091  prmgaplem5  17121  isacs  17713  cidpropd  17772  monpropd  17800  isssc  17883  fullsubc  17913  funcpropd  17965  isfth  17979  fthpropd  17986  grpidpropd  18726  sgrppropd  18795  mndpropd  18823  nmznsg  19240  ghmnsgima  19316  symgextfo  19498  gsmsymgrfixlem1  19503  gsmsymgrfix  19504  fvcosymgeq  19505  gsmsymgreqlem2  19507  psgnunilem3  19572  sylow2blem3  19698  sylow3lem6  19708  cmnpropd  19867  telgsumfzs  20065  rngpropd  20258  ringpropd  20378  c0snmgmhm  20551  abvpropd  20949  lsspropd  21149  lmhmpropd  21205  lbspropd  21231  pj1lmhm  21232  psgndiflemB  21761  phlpropd  21816  islindf  21973  lindfmm  21988  islindf4  21999  islindf5  22000  assapropd  22032  scmatf1  22699  isclo  23255  lmfval  23400  lmconst  23429  iscnrm2  23506  ist0-2  23512  ist1-2  23515  ishaus2  23519  subislly  23649  elpt  23740  elptr  23741  ptbasfi  23749  fclscmp  24198  ufilcmp  24200  cnpfcf  24209  alexsubALTlem1  24215  alexsubALTlem2  24216  alexsubALTlem4  24218  tmdgsum2  24264  tsmsf1o  24313  ustval  24371  ucnval  24444  imasdsf1olem  24541  imasf1oxmet  24543  imasf1omet  24544  metss  24676  prdsxmslem2  24697  lebnumlem3  25133  ishtpy  25142  lmnn  25433  evthicc  25629  cniccbdd  25631  ovolicc2lem4  25690  0pledm  25843  cniccibl  26011  cnicciblnc  26013  c1lip1  26167  lhop1  26184  itgsubstlem  26218  ulmshftlem  26563  ulm0  26565  ulmcau  26569  rlimcnp  27141  fsumdvdsmul  27370  chtub  27387  2sqlem10  27603  dchrisum0flb  27685  pntpbnd1  27761  pntpbnd  27763  pntibndlem2  27766  pntibndlem3  27767  pntibnd  27768  pntlemi  27779  pntleme  27783  pntlem3  27784  pntlemp  27785  pntleml  27786  pnt3  27787  madebdaylemlrcut  28103  noinds  28149  no2indlesm  28158  no3inds  28162  precsexlem9  28419  istrkgld  28739  trgcgrg  28795  tgcgr4  28811  isperp  29003  brbtwn  29260  usgruspgrb  29544  nbgr2vtx1edg  29711  nbuhgr2vtx1edgb  29713  nbgr1vtx  29719  uvtx01vtx  29758  cplgr1v  29791  wlkeq  29994  wlkl1loop  29998  uspgr2wlkeq  30006  upgr2wlk  30027  redwlk  30031  wlkp1lem8  30039  usgr2wlkneq  30116  usgr2trlncl  30120  usgr2pthlem  30123  usgr2pth  30124  pthdlem1  30126  uspgrn2crct  30168  crctcshwlkn0  30181  wwlknp  30203  wwlksn0s  30221  wlkiswwlks1  30227  wlkiswwlks2lem4  30232  wwlksnred  30252  rusgrnumwwlkl1  30331  clwwlkccatlem  30351  clwlkclwwlklem2a1  30354  clwlkclwwlklem2a  30360  clwlkclwwlklem3  30363  clwwlkn  30388  clwwlknp  30399  clwwlkinwwlk  30402  clwwlkn1  30403  clwwlkn2  30406  clwwlkel  30408  clwwlkf  30409  clwwlkwwlksb  30416  1ewlk  30477  upgr3v3e3cycl  30542  upgr4cycl4dv4e  30547  dfconngr1  30550  isconngr1  30552  frgr3v  30637  frgrwopregasn  30678  frgrwopregbsn  30679  ubth  31236  acunirnmpt2  33016  acunirnmpt2f  33017  aciunf1  33019  fnpreimac  33026  fxpgaval  33496  crngmxidl  33761  lmxrge0  34351  measval  34597  isrnmeas  34599  sitgval  34731  eulerpartlemo  34764  eulerpartlemn  34780  onvf1odlem4  35598  subfacp1lem3  35682  subfacp1lem5  35684  txpconn  35732  cvxpconn  35742  cvmscbv  35758  cvmsi  35765  cvmsval  35766  satf  35853  sat1el2xp  35879  elmrsubrn  36020  weiunlem  37002  bj-raldifsn  37770  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  poimirlem32  38331  heicant  38334  mblfinlem3  38338  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  sdclem1  38422  fdc  38424  rrncmslem  38511  isass  38525  isrngod  38577  isgrpda  38634  iscom2  38674  pautsetN  40900  tendofset  41560  tendoset  41561  hdmap14lem13  42682  3factsumint1  42816  sticksstones3  42943  kelac1  43818  gicabl  43854  cantnfresb  44079  safesnsupfilb  44172  fiinfi  44327  clsk1independent  44800  wessf1ornlem  45931  uzub  46173  rexanuz2nf  46234  mccl  46342  climsuse  46352  limsupmnfuzlem  46468  limsupmnfuz  46469  limsupre3uzlem  46477  limsupre3uz  46478  limsupreuz  46479  0cnv  46484  climuz  46486  lmbr3  46489  limsupgt  46520  liminflt  46547  xlimpnfxnegmnf  46556  xlimmnf  46583  xlimpnf  46584  xlimmnfmpt  46585  xlimpnfmpt  46586  dfxlim2  46590  fourierdlem2  46851  fourierdlem3  46852  fourierdlem31  46880  fourierdlem47  46895  fourierdlem70  46918  fourierdlem71  46919  fourierdlem80  46928  fourierdlem103  46951  fourierdlem104  46952  fourierdlem113  46961  etransclem48  47024  etransc  47025  caragenval  47235  omessle  47240  smfmullem2  47534  smfmul  47537  2ffzoeq  48093  iccpval  48192  iccpartigtl  48200  nprmmul1  48304  cycl3grtrilem  48739  grlimedgclnbgr  48788  grlimgrtri  48796  grilcbri2  48804  usgrexmpl2trifr  48830  gpg5nbgrvtx03star  48873  gpg5nbgr3star  48874  lindsrng01  49276  rrx2line  49548  initopropd  50049  termopropd  50050  fucofulem2  50117  thincpropd  50248  isinito2lem  50304