Theorem raleqdv 3321

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

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

This theorem is used by:  raleqtrdv  3323  raleqtrrdv  3325  raleqbidva  3327  raldifeq  4452  frpoinsg  6345  f12dfv  7277  f13dfv  7278  cbvfo  7293  isoselem  7345  ofrfvalg  7689  omsinds  7886  frpoins3xpg  8141  frpoins3xp3g  8142  frrlem4  8291  issmo2  8341  smoeq  8342  on2ind  8660  on3ind  8661  naddsuc2  8693  frfi  9258  marypha1lem  9406  marypha1  9407  dfoi  9486  oieq2  9488  ordtypecbv  9492  ordtypelem2  9494  ordtypelem3  9495  ordtypelem9  9501  wemapwe  9679  ttrclss  9702  ttrclselem2  9708  frinsg  9736  tcrank  9869  scotteqd  9872  isacn  10050  pwsdompw  10208  isfin2  10299  isfin3ds  10334  isf33lem  10371  hsmexlem4  10434  zorn2lem6  10506  zorn2lem7  10507  zorn2g  10508  fpwwe2lem12  10654  uzsupss  12992  fzrevral2  13670  fzrevral3  13671  fzshftral  13672  fzoshftral  13845  uzsinds  14053  expmulnbnd  14301  eqs1  14682  swrdspsleq  14737  pfxeq  14767  pfxsuffeqwrdeq  14769  repswsymballbi  14853  cshw1  14895  pfx2  15020  wwlktovf1  15032  eqwrds3  15036  rexuz3  15438  rexuzre  15442  limsupgle  15566  rlim  15584  climconst  15632  rlimclim1  15634  climshftlem  15663  isercoll  15757  caucvgb  15769  serf0  15770  mertenslem1  15975  coprmprod  16755  coprmproddvds  16757  prmind2  16779  vdwlem10  17086  vdwlem13  17089  vdwnnlem2  17092  vdwnnlem3  17093  vdwnn  17094  ramval  17104  ramz  17121  prmgaplem5  17151  isacs  17743  cidpropd  17802  monpropd  17830  isssc  17913  fullsubc  17943  funcpropd  17995  isfth  18009  fthpropd  18016  grpidpropd  18759  sgrppropd  18835  mndpropd  18866  nmznsg  19292  ghmnsgima  19368  symgextfo  19550  gsmsymgrfixlem1  19555  gsmsymgrfix  19556  fvcosymgeq  19557  gsmsymgreqlem2  19559  psgnunilem3  19624  sylow2blem3  19750  sylow3lem6  19760  cmnpropd  19919  telgsumfzs  20117  rngpropd  20310  ringpropd  20431  c0snmgmhm  20604  abvpropd  21002  lsspropd  21202  lmhmpropd  21258  lbspropd  21284  pj1lmhm  21285  psgndiflemB  21814  phlpropd  21869  islindf  22026  lindfmm  22041  islindf4  22052  islindf5  22053  assapropd  22087  scmatf1  22754  isclo  23313  lmfval  23458  lmconst  23487  iscnrm2  23564  ist0-2  23570  ist1-2  23573  ishaus2  23577  subislly  23708  elpt  23799  elptr  23800  ptbasfi  23808  fclscmp  24257  ufilcmp  24259  cnpfcf  24268  alexsubALTlem1  24274  alexsubALTlem2  24275  alexsubALTlem4  24277  tmdgsum2  24323  tsmsf1o  24372  ustval  24430  ucnval  24503  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  metss  24735  prdsxmslem2  24756  lebnumlem3  25192  ishtpy  25201  lmnn  25492  evthicc  25688  cniccbdd  25690  ovolicc2lem4  25749  0pledm  25902  cniccibl  26070  cnicciblnc  26072  c1lip1  26226  lhop1  26243  itgsubstlem  26277  ulmshftlem  26622  ulm0  26624  ulmcau  26628  rlimcnp  27200  fsumdvdsmul  27429  chtub  27446  2sqlem10  27662  dchrisum0flb  27744  pntpbnd1  27820  pntpbnd  27822  pntibndlem2  27825  pntibndlem3  27826  pntibnd  27827  pntlemi  27838  pntleme  27842  pntlem3  27843  pntlemp  27844  pntleml  27845  pnt3  27846  madebdaylemlrcut  28162  noinds  28208  no2indlesm  28217  no3inds  28221  precsexlem9  28478  istrkgld  28798  trgcgrg  28855  tgcgr4  28871  isperp  29064  brbtwn  29342  usgruspgrb  29629  nbgr2vtx1edg  29796  nbuhgr2vtx1edgb  29798  nbgr1vtx  29804  uvtx01vtx  29843  cplgr1v  29876  wlkeq  30079  wlkl1loop  30083  uspgr2wlkeq  30091  upgr2wlk  30112  redwlk  30116  wlkp1lem8  30124  usgr2wlkneq  30207  usgr2trlncl  30211  usgr2pthlem  30214  usgr2pth  30215  pthdlem1  30217  uspgrn2crct  30262  crctcshwlkn0  30275  wwlknp  30297  wwlksn0s  30315  wlkiswwlks1  30321  wlkiswwlks2lem4  30326  wwlksnred  30346  rusgrnumwwlkl1  30425  clwwlkccatlem  30445  clwlkclwwlklem2a1  30448  clwlkclwwlklem2a  30454  clwlkclwwlklem3  30457  clwwlkn  30482  clwwlknp  30493  clwwlkinwwlk  30496  clwwlkn1  30497  clwwlkn2  30500  clwwlkel  30502  clwwlkf  30503  clwwlkwwlksb  30510  1ewlk  30571  upgr3v3e3cycl  30646  upgr4cycl4dv4e  30651  dfconngr1  30654  isconngr1  30656  frgr3v  30741  frgrwopregasn  30782  frgrwopregbsn  30783  ubth  31340  acunirnmpt2  33120  acunirnmpt2f  33121  aciunf1  33123  fnpreimac  33130  fxpgaval  33594  crngmxidl  33859  lmxrge0  34449  measval  34696  isrnmeas  34698  sitgval  34830  eulerpartlemo  34863  eulerpartlemn  34879  onvf1odlem4  35690  subfacp1lem3  35748  subfacp1lem5  35750  txpconn  35798  cvxpconn  35808  cvmscbv  35824  cvmsi  35831  cvmsval  35832  satf  35919  sat1el2xp  35945  elmrsubrn  36086  weiunlem  37069  bj-raldifsn  37837  poimirlem26  38382  poimirlem27  38383  poimirlem31  38387  poimirlem32  38388  heicant  38391  mblfinlem3  38395  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  sdclem1  38480  fdc  38482  rrncmslem  38569  isass  38583  isrngod  38635  isgrpda  38692  iscom2  38732  pautsetN  40958  tendofset  41618  tendoset  41619  hdmap14lem13  42740  3factsumint1  42874  sticksstones3  43001  kelac1  43891  gicabl  43927  cantnfresb  44152  safesnsupfilb  44245  fiinfi  44400  clsk1independent  44873  wessf1ornlem  46004  uzub  46246  rexanuz2nf  46307  mccl  46415  climsuse  46425  limsupmnfuzlem  46541  limsupmnfuz  46542  limsupre3uzlem  46550  limsupre3uz  46551  limsupreuz  46552  0cnv  46557  climuz  46559  lmbr3  46562  limsupgt  46593  liminflt  46620  xlimpnfxnegmnf  46629  xlimmnf  46656  xlimpnf  46657  xlimmnfmpt  46658  xlimpnfmpt  46659  dfxlim2  46663  fourierdlem2  46924  fourierdlem3  46925  fourierdlem31  46953  fourierdlem47  46968  fourierdlem70  46991  fourierdlem71  46992  fourierdlem80  47001  fourierdlem103  47024  fourierdlem104  47025  fourierdlem113  47034  etransclem48  47097  etransc  47098  caragenval  47308  omessle  47313  smfmullem2  47607  smfmul  47610  2ffzoeq  48203  iccpval  48302  iccpartigtl  48310  nprmmul1  48414  cycl3grtrilem  48849  grlimedgclnbgr  48898  grlimgrtri  48906  grilcbri2  48914  usgrexmpl2trifr  48940  gpg5nbgrvtx03star  48983  gpg5nbgr3star  48984  lindsrng01  49385  rrx2line  49657  initopropd  50156  termopropd  50157  fucofulem2  50224  thincpropd  50355  isinito2lem  50411