Theorem raleqdv 3334

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ral 3068  df-rex 3077

This theorem is referenced by:  raleqtrdv  3336  raleqtrrdv  3338  raleqbidva  3340  raleleqOLD  3351  raldifeq  4517  frpoinsg  6375  wfisgOLD  6386  f12dfv  7309  f13dfv  7310  cbvfo  7325  isoselem  7377  ofrfvalg  7722  omsinds  7924  omsindsOLD  7925  frpoins3xpg  8181  frpoins3xp3g  8182  frrlem4  8330  wfrlem4OLD  8368  issmo2  8405  smoeq  8406  on2ind  8725  on3ind  8726  naddsuc2  8757  frfi  9349  marypha1lem  9502  marypha1  9503  dfoi  9580  oieq2  9582  ordtypecbv  9586  ordtypelem2  9588  ordtypelem3  9589  ordtypelem9  9595  wemapwe  9766  ttrclss  9789  ttrclselem2  9795  frinsg  9820  tcrank  9953  isacn  10113  pwsdompw  10272  isfin2  10363  isfin3ds  10398  isf33lem  10435  hsmexlem4  10498  zorn2lem6  10570  zorn2lem7  10571  zorn2g  10572  fpwwe2lem12  10711  uzsupss  13005  fzrevral2  13670  fzrevral3  13671  fzshftral  13672  fzoshftral  13834  uzsinds  14038  expmulnbnd  14284  eqs1  14660  swrdspsleq  14713  pfxeq  14744  pfxsuffeqwrdeq  14746  repswsymballbi  14828  cshw1  14870  pfx2  14996  wwlktovf1  15006  eqwrds3  15010  rexuz3  15397  rexuzre  15401  limsupgle  15523  rlim  15541  climconst  15589  rlimclim1  15591  climshftlem  15620  isercoll  15716  caucvgb  15728  serf0  15729  mertenslem1  15932  coprmprod  16708  coprmproddvds  16710  prmind2  16732  vdwlem10  17037  vdwlem13  17040  vdwnnlem2  17043  vdwnnlem3  17044  vdwnn  17045  ramval  17055  ramz  17072  prmgaplem5  17102  isacs  17709  cidpropd  17768  monpropd  17798  isssc  17881  fullsubc  17914  funcpropd  17967  isfth  17981  fthpropd  17988  grpidpropd  18700  sgrppropd  18769  mndpropd  18797  nmznsg  19208  ghmnsgima  19280  symgextfo  19464  gsmsymgrfixlem1  19469  gsmsymgrfix  19470  fvcosymgeq  19471  gsmsymgreqlem2  19473  psgnunilem3  19538  sylow2blem3  19664  sylow3lem6  19674  cmnpropd  19833  telgsumfzs  20031  rngpropd  20201  ringpropd  20311  c0snmgmhm  20488  abvpropd  20858  lsspropd  21039  lmhmpropd  21095  lbspropd  21121  pj1lmhm  21122  psgndiflemB  21641  phlpropd  21696  islindf  21855  lindfmm  21870  islindf4  21881  islindf5  21882  assapropd  21915  scmatf1  22558  isclo  23116  lmfval  23261  lmconst  23290  iscnrm2  23367  ist0-2  23373  ist1-2  23376  ishaus2  23380  subislly  23510  elpt  23601  elptr  23602  ptbasfi  23610  fclscmp  24059  ufilcmp  24061  cnpfcf  24070  alexsubALTlem1  24076  alexsubALTlem2  24077  alexsubALTlem4  24079  tmdgsum2  24125  tsmsf1o  24174  ustval  24232  ucnval  24307  imasdsf1olem  24404  imasf1oxmet  24406  imasf1omet  24407  metss  24542  prdsxmslem2  24563  lebnumlem3  25014  ishtpy  25023  lmnn  25316  evthicc  25513  cniccbdd  25515  ovolicc2lem4  25574  0pledm  25727  cniccibl  25896  cnicciblnc  25898  c1lip1  26056  lhop1  26073  itgsubstlem  26109  ulmshftlem  26450  ulm0  26452  ulmcau  26456  rlimcnp  27026  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  chtub  27274  2sqlem10  27490  dchrisum0flb  27572  pntpbnd1  27648  pntpbnd  27650  pntibndlem2  27653  pntibndlem3  27654  pntibnd  27655  pntlemi  27666  pntleme  27670  pntlem3  27671  pntlemp  27672  pntleml  27673  pnt3  27674  madebdaylemlrcut  27955  noinds  27996  no2indslem  28005  no3inds  28009  precsexlem9  28257  istrkgld  28485  trgcgrg  28541  tgcgr4  28557  isperp  28738  brbtwn  28932  usgruspgrb  29218  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nbgr1vtx  29393  uvtx01vtx  29432  cplgr1v  29465  wlkeq  29670  wlkl1loop  29674  uspgr2wlkeq  29682  upgr2wlk  29704  redwlk  29708  wlkp1lem8  29716  usgr2wlkneq  29792  usgr2trlncl  29796  usgr2pthlem  29799  usgr2pth  29800  pthdlem1  29802  uspgrn2crct  29841  crctcshwlkn0  29854  wwlknp  29876  wwlksn0s  29894  wlkiswwlks1  29900  wlkiswwlks2lem4  29905  wwlksnred  29925  rusgrnumwwlkl1  30001  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwwlkn  30058  clwwlknp  30069  clwwlkinwwlk  30072  clwwlkn1  30073  clwwlkn2  30076  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  1ewlk  30147  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  dfconngr1  30220  isconngr1  30222  frgr3v  30307  frgrwopregasn  30348  frgrwopregbsn  30349  ubth  30905  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1  32681  fnpreimac  32689  crngmxidl  33462  lmxrge0  33898  measval  34162  isrnmeas  34164  sitgval  34297  eulerpartlemo  34330  eulerpartlemn  34346  subfacp1lem3  35150  subfacp1lem5  35152  txpconn  35200  cvxpconn  35210  cvmscbv  35226  cvmsi  35233  cvmsval  35234  satf  35321  sat1el2xp  35347  elmrsubrn  35488  weiunlem2  36429  bj-raldifsn  37066  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  heicant  37615  mblfinlem3  37619  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  sdclem1  37703  fdc  37705  rrncmslem  37792  isass  37806  isrngod  37858  isgrpda  37915  iscom2  37955  pautsetN  40055  tendofset  40715  tendoset  40716  hdmap14lem13  41837  3factsumint1  41978  sticksstones3  42105  kelac1  43020  gicabl  43056  cantnfresb  43286  safesnsupfilb  43380  fiinfi  43535  clsk1independent  44008  scotteqd  44206  wessf1ornlem  45092  uzub  45346  rexanuz2nf  45408  mccl  45519  climsuse  45529  limsupmnfuzlem  45647  limsupmnfuz  45648  limsupre3uzlem  45656  limsupre3uz  45657  limsupreuz  45658  0cnv  45663  climuz  45665  lmbr3  45668  limsupgt  45699  liminflt  45726  xlimpnfxnegmnf  45735  xlimmnf  45762  xlimpnf  45763  xlimmnfmpt  45764  xlimpnfmpt  45765  dfxlim2  45769  fourierdlem2  46030  fourierdlem3  46031  fourierdlem31  46059  fourierdlem47  46074  fourierdlem70  46097  fourierdlem71  46098  fourierdlem80  46107  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  etransclem48  46203  etransc  46204  caragenval  46414  omessle  46419  smfmullem2  46713  smfmul  46716  2ffzoeq  47242  iccpval  47289  iccpartigtl  47297  grlimgrtri  47820  grilcbri2  47828  usgrexmpl2trifr  47852  lindsrng01  48197  rrx2line  48474