Theorem raleqdv 3325

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∀wral 3061

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ral 3062  df-rex 3071

This theorem is referenced by:  raleqbidva  3327  raleleqALT  3341  raldifeq  4492  frpoinsg  6341  wfisgOLD  6352  fveqressseq  7078  f12dfv  7267  f13dfv  7268  cbvfo  7283  isoselem  7334  ofrfvalg  7674  omsinds  7872  omsindsOLD  7873  frpoins3xpg  8122  frpoins3xp3g  8123  frrlem4  8270  wfrlem4OLD  8308  issmo2  8345  smoeq  8346  on2ind  8664  on3ind  8665  frfi  9284  marypha1lem  9424  marypha1  9425  dfoi  9502  oieq2  9504  ordtypecbv  9508  ordtypelem2  9510  ordtypelem3  9511  ordtypelem9  9517  wemapwe  9688  ttrclss  9711  ttrclselem2  9717  frinsg  9742  tcrank  9875  isacn  10035  pwsdompw  10195  isfin2  10285  isfin3ds  10320  isf33lem  10357  hsmexlem4  10420  zorn2lem6  10492  zorn2lem7  10493  zorn2g  10494  fpwwe2lem12  10633  uzsupss  12920  fzrevral2  13583  fzrevral3  13584  fzshftral  13585  fzoshftral  13745  uzsinds  13948  expmulnbnd  14194  eqs1  14558  swrdspsleq  14611  pfxeq  14642  pfxsuffeqwrdeq  14644  repswsymballbi  14726  cshw1  14768  pfx2  14894  wwlktovf1  14904  eqwrds3  14908  rexuz3  15291  rexuzre  15295  limsupgle  15417  rlim  15435  climconst  15483  rlimclim1  15485  climshftlem  15514  isercoll  15610  caucvgb  15622  serf0  15623  mertenslem1  15826  coprmprod  16594  coprmproddvds  16596  prmind2  16618  vdwlem10  16919  vdwlem13  16922  vdwnnlem2  16925  vdwnnlem3  16926  vdwnn  16927  ramval  16937  ramz  16954  prmgaplem5  16984  isacs  17591  cidpropd  17650  monpropd  17680  isssc  17763  fullsubc  17796  funcpropd  17847  isfth  17861  fthpropd  17868  grpidpropd  18577  sgrppropd  18618  mndpropd  18646  nmznsg  19042  ghmnsgima  19110  symgextfo  19284  gsmsymgrfixlem1  19289  gsmsymgrfix  19290  fvcosymgeq  19291  gsmsymgreqlem2  19293  symgfixf1  19299  psgnunilem3  19358  subgpgp  19459  sylow2blem3  19484  sylow3lem6  19494  efgsp1  19599  efgsres  19600  cmnpropd  19653  telgsumfzs  19851  ablfac2  19953  ringpropd  20095  abvpropd  20442  lsspropd  20620  lmhmpropd  20676  lbspropd  20702  pj1lmhm  20703  znf1o  21098  psgndiflemB  21144  phlpropd  21199  islindf  21358  lindfmm  21373  islindf4  21384  islindf5  21385  assapropd  21417  scmatf1  22024  isclo  22582  perfopn  22680  lmfval  22727  lmconst  22756  cncnp  22775  iscnrm2  22833  ist0-2  22839  ist1-2  22842  ishaus2  22846  ordtt1  22874  subislly  22976  elpt  23067  elptr  23068  ptbasfi  23076  tx1stc  23145  xkococnlem  23154  fclscmp  23525  ufilcmp  23527  cnpfcf  23536  alexsubALTlem1  23542  alexsubALTlem2  23543  alexsubALTlem4  23545  tmdgsum2  23591  tsmsf1o  23640  ustval  23698  ucnval  23773  imasdsf1olem  23870  imasf1oxmet  23872  imasf1omet  23873  metss  24008  prdsxmslem2  24029  cnmpopc  24435  lebnumlem3  24470  ishtpy  24479  pi1coghm  24568  lmnn  24771  evthicc  24967  cniccbdd  24969  ovolicc2lem4  25028  0pledm  25181  cniccibl  25349  cnicciblnc  25351  c1lip1  25505  dvivthlem1  25516  lhop1  25522  itgsubstlem  25556  dgrlem  25734  ulmshftlem  25892  ulm0  25894  ulmcau  25898  iblulm  25910  rlimcnp  26459  xrlimcnp  26462  fsumdvdsmul  26688  chtub  26704  2sqlem10  26920  dchrisum0flb  27002  pntpbnd1  27078  pntpbnd  27080  pntibndlem2  27083  pntibndlem3  27084  pntibnd  27085  pntlemi  27096  pntleme  27100  pntlem3  27101  pntlemp  27102  pntleml  27103  pnt3  27104  madebdaylemlrcut  27382  noinds  27418  no2indslem  27427  no3inds  27431  precsexlem9  27650  istrkgld  27699  trgcgrg  27755  tgcgr4  27771  isperp  27952  brbtwn  28146  usgruspgrb  28430  usgr1e  28491  nbgr2vtx1edg  28596  nbuhgr2vtx1edgb  28598  nbgr0vtx  28602  nbgr1vtx  28604  uvtx01vtx  28643  cplgr1v  28676  cusgrexi  28689  1hevtxdg0  28751  wlkeq  28880  wlkl1loop  28884  uspgr2wlkeq  28892  upgr2wlk  28914  redwlk  28918  wlkp1lem8  28926  usgr2wlkneq  29002  usgr2trlncl  29006  usgr2pthlem  29009  usgr2pth  29010  pthdlem1  29012  uspgrn2crct  29051  crctcshwlkn0lem7  29059  crctcshwlkn0  29064  wwlknp  29086  wwlksn0s  29104  wlkiswwlks1  29110  wlkiswwlks2lem4  29115  wlkiswwlksupgr2  29120  wlknewwlksn  29130  wwlksnred  29135  wwlksnext  29136  rusgrnumwwlkl1  29211  clwwlkccatlem  29231  clwlkclwwlklem2a1  29234  clwlkclwwlklem2a  29240  clwlkclwwlklem3  29243  clwlkclwwlkf1lem3  29248  clwwlkn  29268  clwwlknp  29279  clwwlkinwwlk  29282  clwwlkn1  29283  clwwlkn2  29286  clwwlkel  29288  clwwlkf  29289  clwwlkwwlksb  29296  wwlksext2clwwlk  29299  wwlksubclwwlk  29300  clwwlknonex2  29351  1ewlk  29357  1wlkdlem4  29382  upgr3v3e3cycl  29422  upgr4cycl4dv4e  29427  dfconngr1  29430  isconngr1  29432  frgr3v  29517  frgrwopregasn  29558  frgrwopregbsn  29559  ubth  30113  acunirnmpt2  31872  acunirnmpt2f  31873  aciunf1  31875  fnpreimac  31883  crngmxidl  32573  lmxrge0  32920  sigaclcu3  33108  measval  33184  isrnmeas  33186  sitgval  33319  eulerpartlemsv3  33348  eulerpartlemo  33352  eulerpartlemn  33368  bnj1514  34062  subfacp1lem3  34161  subfacp1lem5  34163  txpconn  34211  cvxpconn  34221  cvmscbv  34237  cvmsi  34244  cvmsval  34245  satf  34332  sat1el2xp  34358  elmrsubrn  34499  bj-raldifsn  35969  poimirlem1  36477  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  poimirlem32  36508  heicant  36511  mblfinlem3  36515  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  sdclem1  36599  fdc  36601  rrncmslem  36688  isass  36702  exidreslem  36733  exidresid  36735  isrngod  36754  isgrpda  36811  iscom2  36851  pautsetN  38957  tendofset  39617  tendoset  39618  hdmap14lem13  40739  3factsumint1  40874  sticksstones3  40952  kelac1  41790  gicabl  41826  lpirlnr  41844  cantnfresb  42059  oaun3lem1  42109  naddsuc2  42128  safesnsupfilb  42154  fiinfi  42309  clsk1independent  42782  scotteqd  42981  wessf1ornlem  43867  uzub  44127  rexanuz2nf  44189  mccl  44300  climsuse  44310  limsupmnfuzlem  44428  limsupmnfuz  44429  limsupre3uzlem  44437  limsupre3uz  44438  limsupreuz  44439  0cnv  44444  climuz  44446  lmbr3  44449  limsupgt  44480  liminflt  44507  xlimpnfxnegmnf  44516  xlimmnf  44543  xlimpnf  44544  xlimmnfmpt  44545  xlimpnfmpt  44546  dfxlim2  44550  fourierdlem2  44811  fourierdlem3  44812  fourierdlem31  44840  fourierdlem47  44855  fourierdlem70  44878  fourierdlem71  44879  fourierdlem73  44881  fourierdlem80  44888  fourierdlem103  44911  fourierdlem104  44912  fourierdlem113  44921  etransclem48  44984  etransc  44985  caragenval  45195  omessle  45200  smfmullem2  45494  smfmul  45497  2ffzoeq  46022  iccpval  46069  iccpartigtl  46077  rngpropd  46659  c0snmgmhm  46698  linds0  47099  lindsrng01  47102  rrx2line  47379