Theorem raleqdv 3309

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ral 3053  df-rex 3062

This theorem is referenced by:  raleqtrdv  3311  raleqtrrdv  3313  raleqbidva  3315  raleleqOLD  3326  raldifeq  4474  frpoinsg  6337  wfisgOLD  6348  f12dfv  7271  f13dfv  7272  cbvfo  7287  isoselem  7339  ofrfvalg  7684  omsinds  7887  frpoins3xpg  8144  frpoins3xp3g  8145  frrlem4  8293  wfrlem4OLD  8331  issmo2  8368  smoeq  8369  on2ind  8686  on3ind  8687  naddsuc2  8718  frfi  9298  marypha1lem  9450  marypha1  9451  dfoi  9530  oieq2  9532  ordtypecbv  9536  ordtypelem2  9538  ordtypelem3  9539  ordtypelem9  9545  wemapwe  9716  ttrclss  9739  ttrclselem2  9745  frinsg  9770  tcrank  9903  isacn  10063  pwsdompw  10222  isfin2  10313  isfin3ds  10348  isf33lem  10385  hsmexlem4  10448  zorn2lem6  10520  zorn2lem7  10521  zorn2g  10522  fpwwe2lem12  10661  uzsupss  12961  fzrevral2  13635  fzrevral3  13636  fzshftral  13637  fzoshftral  13805  uzsinds  14010  expmulnbnd  14258  eqs1  14635  swrdspsleq  14688  pfxeq  14719  pfxsuffeqwrdeq  14721  repswsymballbi  14803  cshw1  14845  pfx2  14971  wwlktovf1  14981  eqwrds3  14985  rexuz3  15372  rexuzre  15376  limsupgle  15498  rlim  15516  climconst  15564  rlimclim1  15566  climshftlem  15595  isercoll  15689  caucvgb  15701  serf0  15702  mertenslem1  15905  coprmprod  16685  coprmproddvds  16687  prmind2  16709  vdwlem10  17015  vdwlem13  17018  vdwnnlem2  17021  vdwnnlem3  17022  vdwnn  17023  ramval  17033  ramz  17050  prmgaplem5  17080  isacs  17668  cidpropd  17727  monpropd  17755  isssc  17838  fullsubc  17868  funcpropd  17920  isfth  17934  fthpropd  17941  grpidpropd  18645  sgrppropd  18714  mndpropd  18742  nmznsg  19156  ghmnsgima  19228  symgextfo  19408  gsmsymgrfixlem1  19413  gsmsymgrfix  19414  fvcosymgeq  19415  gsmsymgreqlem2  19417  psgnunilem3  19482  sylow2blem3  19608  sylow3lem6  19618  cmnpropd  19777  telgsumfzs  19975  rngpropd  20139  ringpropd  20253  c0snmgmhm  20427  abvpropd  20800  lsspropd  20980  lmhmpropd  21036  lbspropd  21062  pj1lmhm  21063  psgndiflemB  21565  phlpropd  21620  islindf  21777  lindfmm  21792  islindf4  21803  islindf5  21804  assapropd  21837  scmatf1  22474  isclo  23030  lmfval  23175  lmconst  23204  iscnrm2  23281  ist0-2  23287  ist1-2  23290  ishaus2  23294  subislly  23424  elpt  23515  elptr  23516  ptbasfi  23524  fclscmp  23973  ufilcmp  23975  cnpfcf  23984  alexsubALTlem1  23990  alexsubALTlem2  23991  alexsubALTlem4  23993  tmdgsum2  24039  tsmsf1o  24088  ustval  24146  ucnval  24220  imasdsf1olem  24317  imasf1oxmet  24319  imasf1omet  24320  metss  24452  prdsxmslem2  24473  lebnumlem3  24918  ishtpy  24927  lmnn  25220  evthicc  25417  cniccbdd  25419  ovolicc2lem4  25478  0pledm  25631  cniccibl  25799  cnicciblnc  25801  c1lip1  25959  lhop1  25976  itgsubstlem  26012  ulmshftlem  26355  ulm0  26357  ulmcau  26361  rlimcnp  26932  fsumdvdsmul  27162  fsumdvdsmulOLD  27164  chtub  27180  2sqlem10  27396  dchrisum0flb  27478  pntpbnd1  27554  pntpbnd  27556  pntibndlem2  27559  pntibndlem3  27560  pntibnd  27561  pntlemi  27572  pntleme  27576  pntlem3  27577  pntlemp  27578  pntleml  27579  pnt3  27580  madebdaylemlrcut  27867  noinds  27909  no2indslem  27918  no3inds  27922  precsexlem9  28174  istrkgld  28443  trgcgrg  28499  tgcgr4  28515  isperp  28696  brbtwn  28883  usgruspgrb  29167  nbgr2vtx1edg  29334  nbuhgr2vtx1edgb  29336  nbgr1vtx  29342  uvtx01vtx  29381  cplgr1v  29414  wlkeq  29619  wlkl1loop  29623  uspgr2wlkeq  29631  upgr2wlk  29653  redwlk  29657  wlkp1lem8  29665  usgr2wlkneq  29743  usgr2trlncl  29747  usgr2pthlem  29750  usgr2pth  29751  pthdlem1  29753  uspgrn2crct  29795  crctcshwlkn0  29808  wwlknp  29830  wwlksn0s  29848  wlkiswwlks1  29854  wlkiswwlks2lem4  29859  wwlksnred  29879  rusgrnumwwlkl1  29955  clwwlkccatlem  29975  clwlkclwwlklem2a1  29978  clwlkclwwlklem2a  29984  clwlkclwwlklem3  29987  clwwlkn  30012  clwwlknp  30023  clwwlkinwwlk  30026  clwwlkn1  30027  clwwlkn2  30030  clwwlkel  30032  clwwlkf  30033  clwwlkwwlksb  30040  1ewlk  30101  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  dfconngr1  30174  isconngr1  30176  frgr3v  30261  frgrwopregasn  30302  frgrwopregbsn  30303  ubth  30859  acunirnmpt2  32643  acunirnmpt2f  32644  aciunf1  32646  fnpreimac  32654  crngmxidl  33489  lmxrge0  33988  measval  34234  isrnmeas  34236  sitgval  34369  eulerpartlemo  34402  eulerpartlemn  34418  subfacp1lem3  35209  subfacp1lem5  35211  txpconn  35259  cvxpconn  35269  cvmscbv  35285  cvmsi  35292  cvmsval  35293  satf  35380  sat1el2xp  35406  elmrsubrn  35547  weiunlem2  36486  bj-raldifsn  37123  poimirlem26  37675  poimirlem27  37676  poimirlem31  37680  poimirlem32  37681  heicant  37684  mblfinlem3  37688  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  sdclem1  37772  fdc  37774  rrncmslem  37861  isass  37875  isrngod  37927  isgrpda  37984  iscom2  38024  pautsetN  40122  tendofset  40782  tendoset  40783  hdmap14lem13  41904  3factsumint1  42039  sticksstones3  42166  kelac1  43062  gicabl  43098  cantnfresb  43323  safesnsupfilb  43417  fiinfi  43572  clsk1independent  44045  scotteqd  44236  wessf1ornlem  45189  uzub  45438  rexanuz2nf  45499  mccl  45607  climsuse  45617  limsupmnfuzlem  45735  limsupmnfuz  45736  limsupre3uzlem  45744  limsupre3uz  45745  limsupreuz  45746  0cnv  45751  climuz  45753  lmbr3  45756  limsupgt  45787  liminflt  45814  xlimpnfxnegmnf  45823  xlimmnf  45850  xlimpnf  45851  xlimmnfmpt  45852  xlimpnfmpt  45853  dfxlim2  45857  fourierdlem2  46118  fourierdlem3  46119  fourierdlem31  46147  fourierdlem47  46162  fourierdlem70  46185  fourierdlem71  46186  fourierdlem80  46195  fourierdlem103  46218  fourierdlem104  46219  fourierdlem113  46228  etransclem48  46291  etransc  46292  caragenval  46502  omessle  46507  smfmullem2  46801  smfmul  46804  2ffzoeq  47336  iccpval  47409  iccpartigtl  47417  cycl3grtrilem  47938  grlimgrtri  47988  grilcbri2  47996  usgrexmpl2trifr  48021  gpg5nbgrvtx03star  48062  gpg5nbgr3star  48063  lindsrng01  48424  rrx2line  48700  initopropd  49140  termopropd  49141  fucofulem2  49202  thincpropd  49308  isinito2lem  49363