Theorem raleqdv 3295

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

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

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 2708

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

This theorem is referenced by:  raleqtrdv  3297  raleqtrrdv  3299  raleqbidva  3301  raleleqOLD  3308  raldifeq  4433  frpoinsg  6307  f12dfv  7228  f13dfv  7229  cbvfo  7244  isoselem  7296  ofrfvalg  7639  omsinds  7838  frpoins3xpg  8090  frpoins3xp3g  8091  frrlem4  8239  issmo2  8289  smoeq  8290  on2ind  8605  on3ind  8606  naddsuc2  8637  frfi  9195  marypha1lem  9346  marypha1  9347  dfoi  9426  oieq2  9428  ordtypecbv  9432  ordtypelem2  9434  ordtypelem3  9435  ordtypelem9  9441  wemapwe  9618  ttrclss  9641  ttrclselem2  9647  frinsg  9675  tcrank  9808  isacn  9966  pwsdompw  10125  isfin2  10216  isfin3ds  10251  isf33lem  10288  hsmexlem4  10351  zorn2lem6  10423  zorn2lem7  10424  zorn2g  10425  fpwwe2lem12  10565  uzsupss  12890  fzrevral2  13567  fzrevral3  13568  fzshftral  13569  fzoshftral  13742  uzsinds  13949  expmulnbnd  14197  eqs1  14575  swrdspsleq  14628  pfxeq  14658  pfxsuffeqwrdeq  14660  repswsymballbi  14742  cshw1  14784  pfx2  14909  wwlktovf1  14919  eqwrds3  14923  rexuz3  15311  rexuzre  15315  limsupgle  15439  rlim  15457  climconst  15505  rlimclim1  15507  climshftlem  15536  isercoll  15630  caucvgb  15642  serf0  15643  mertenslem1  15849  coprmprod  16630  coprmproddvds  16632  prmind2  16654  vdwlem10  16961  vdwlem13  16964  vdwnnlem2  16967  vdwnnlem3  16968  vdwnn  16969  ramval  16979  ramz  16996  prmgaplem5  17026  isacs  17617  cidpropd  17676  monpropd  17704  isssc  17787  fullsubc  17817  funcpropd  17869  isfth  17883  fthpropd  17890  grpidpropd  18630  sgrppropd  18699  mndpropd  18727  nmznsg  19143  ghmnsgima  19215  symgextfo  19397  gsmsymgrfixlem1  19402  gsmsymgrfix  19403  fvcosymgeq  19404  gsmsymgreqlem2  19406  psgnunilem3  19471  sylow2blem3  19597  sylow3lem6  19607  cmnpropd  19766  telgsumfzs  19964  rngpropd  20155  ringpropd  20269  c0snmgmhm  20442  abvpropd  20812  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  pj1lmhm  21095  psgndiflemB  21580  phlpropd  21635  islindf  21792  lindfmm  21807  islindf4  21818  islindf5  21819  assapropd  21851  scmatf1  22496  isclo  23052  lmfval  23197  lmconst  23226  iscnrm2  23303  ist0-2  23309  ist1-2  23312  ishaus2  23316  subislly  23446  elpt  23537  elptr  23538  ptbasfi  23546  fclscmp  23995  ufilcmp  23997  cnpfcf  24006  alexsubALTlem1  24012  alexsubALTlem2  24013  alexsubALTlem4  24015  tmdgsum2  24061  tsmsf1o  24110  ustval  24168  ucnval  24241  imasdsf1olem  24338  imasf1oxmet  24340  imasf1omet  24341  metss  24473  prdsxmslem2  24494  lebnumlem3  24930  ishtpy  24939  lmnn  25230  evthicc  25426  cniccbdd  25428  ovolicc2lem4  25487  0pledm  25640  cniccibl  25808  cnicciblnc  25810  c1lip1  25964  lhop1  25981  itgsubstlem  26015  ulmshftlem  26354  ulm0  26356  ulmcau  26360  rlimcnp  26929  fsumdvdsmul  27158  chtub  27175  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  pntpbnd  27551  pntibndlem2  27554  pntibndlem3  27555  pntibnd  27556  pntlemi  27567  pntleme  27571  pntlem3  27572  pntlemp  27573  pntleml  27574  pnt3  27575  madebdaylemlrcut  27891  noinds  27937  no2indlesm  27946  no3inds  27950  precsexlem9  28207  istrkgld  28527  trgcgrg  28583  tgcgr4  28599  isperp  28780  brbtwn  28968  usgruspgrb  29252  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nbgr1vtx  29427  uvtx01vtx  29466  cplgr1v  29499  wlkeq  29702  wlkl1loop  29706  uspgr2wlkeq  29714  upgr2wlk  29735  redwlk  29739  wlkp1lem8  29747  usgr2wlkneq  29824  usgr2trlncl  29828  usgr2pthlem  29831  usgr2pth  29832  pthdlem1  29834  uspgrn2crct  29876  crctcshwlkn0  29889  wwlknp  29911  wwlksn0s  29929  wlkiswwlks1  29935  wlkiswwlks2lem4  29940  wwlksnred  29960  rusgrnumwwlkl1  30039  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a  30068  clwlkclwwlklem3  30071  clwwlkn  30096  clwwlknp  30107  clwwlkinwwlk  30110  clwwlkn1  30111  clwwlkn2  30114  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  1ewlk  30185  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  dfconngr1  30258  isconngr1  30260  frgr3v  30345  frgrwopregasn  30386  frgrwopregbsn  30387  ubth  30944  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1  32736  fnpreimac  32743  fxpgaval  33228  crngmxidl  33529  lmxrge0  34096  measval  34342  isrnmeas  34344  sitgval  34476  eulerpartlemo  34509  eulerpartlemn  34525  onvf1odlem4  35288  subfacp1lem3  35364  subfacp1lem5  35366  txpconn  35414  cvxpconn  35424  cvmscbv  35440  cvmsi  35447  cvmsval  35448  satf  35535  sat1el2xp  35561  elmrsubrn  35702  weiunlem  36645  bj-raldifsn  37412  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  heicant  37976  mblfinlem3  37980  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  sdclem1  38064  fdc  38066  rrncmslem  38153  isass  38167  isrngod  38219  isgrpda  38276  iscom2  38316  pautsetN  40544  tendofset  41204  tendoset  41205  hdmap14lem13  42326  3factsumint1  42460  sticksstones3  42587  kelac1  43491  gicabl  43527  cantnfresb  43752  safesnsupfilb  43845  fiinfi  44000  clsk1independent  44473  scotteqd  44664  wessf1ornlem  45615  uzub  45859  rexanuz2nf  45920  mccl  46028  climsuse  46038  limsupmnfuzlem  46154  limsupmnfuz  46155  limsupre3uzlem  46163  limsupre3uz  46164  limsupreuz  46165  0cnv  46170  climuz  46172  lmbr3  46175  limsupgt  46206  liminflt  46233  xlimpnfxnegmnf  46242  xlimmnf  46269  xlimpnf  46270  xlimmnfmpt  46271  xlimpnfmpt  46272  dfxlim2  46276  fourierdlem2  46537  fourierdlem3  46538  fourierdlem31  46566  fourierdlem47  46581  fourierdlem70  46604  fourierdlem71  46605  fourierdlem80  46614  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  etransclem48  46710  etransc  46711  caragenval  46921  omessle  46926  smfmullem2  47220  smfmul  47223  2ffzoeq  47776  iccpval  47875  iccpartigtl  47883  nprmmul1  47987  cycl3grtrilem  48422  grlimedgclnbgr  48471  grlimgrtri  48479  grilcbri2  48487  usgrexmpl2trifr  48513  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  lindsrng01  48944  rrx2line  49216  initopropd  49718  termopropd  49719  fucofulem2  49786  thincpropd  49917  isinito2lem  49973