MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq12d Structured version   Unicode version

Theorem eqeq12d 2450
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1  |-  ( ph  ->  A  =  B )
eqeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eqeq12d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 eqeq12 2448 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652
This theorem is referenced by:  cdeqeq  3156  sbceqg  3267  csbing  3548  csbifg  3767  uniprg  4030  unisng  4032  intprg  4084  iununi  4175  csbopabg  4283  limeq  4593  ordunisuc  4812  onsucuni2  4814  orduninsuc  4823  csbima12g  5213  dmsnsnsn  5348  cnvsng  5355  csbiotag  5447  csbfv12gALT  5739  fveqres  5764  fvmptf  5821  eqfnfv2f  5831  fvreseq  5833  fmptco  5901  fnressn  5918  fvsng  5927  fnpr  5950  fnprOLD  5951  fnsuppres  5952  cocan1  6024  cocan2  6025  fliftfun  6034  weniso  6075  csbovg  6112  eqfnov  6176  ovmpt2s  6197  ov2gf  6198  ovmpt2dxf  6199  caovcomg  6242  caovassg  6245  caovcang  6248  caovcanrd  6250  caovcan  6251  caovdig  6261  caovdirg  6264  caovmo  6284  grprinvlem  6285  grprinvd  6286  offveqb  6326  caofid0l  6332  caofid0r  6333  caofass  6338  caonncan  6342  op1stg  6359  op2ndg  6360  f1o2ndf1  6454  opabiota  6538  csbriotag  6562  onfununi  6603  tfrlem1  6636  tfrlem2  6637  tfrlem3  6638  tfrlem3a  6639  tfrlem9  6646  tfrlem11  6649  tfrlem12  6650  tfr3  6660  tz7.44-1  6664  tz7.44-2  6665  tz7.44-3  6666  rdglem1  6673  rdg0g  6685  seqomlem1  6707  abianfp  6716  oalim  6776  omlim  6777  oelim  6778  oa0r  6782  om0r  6783  om1r  6786  oaass  6804  oarec  6805  odi  6822  omass  6823  oelim2  6838  oeoalem  6839  oeoa  6840  oeoelem  6841  oeoe  6842  nna0r  6852  nnacom  6860  nnaass  6865  nndi  6866  nnmass  6867  nnmsucr  6868  nnmcom  6869  oaabs  6887  oaabs2  6888  omabs  6890  ecovcom  7015  ecovass  7016  ecovdi  7017  dom2lem  7147  unxpdomlem2  7314  unxpdomlem3  7315  ixpfi2  7405  fipreima  7412  ordiso2  7484  wemaplem1  7515  wemaplem2  7516  wemapso2lem  7519  cantnfval2  7624  cantnfp1lem3  7636  oemapvali  7640  cantnflem1c  7643  cantnflem1  7645  wemapwe  7654  tcvalg  7677  rankvalg  7743  rankonidlem  7754  ranklim  7770  rankuni  7789  cardprclem  7866  cardprc  7867  carduni  7868  fseqenlem1  7905  fodomacn  7937  alephcard  7951  alephfp2  7990  alephval3  7991  dfac12lem1  8023  dfac12lem2  8024  dfac12r  8026  ackbij1lem5  8104  ackbij1lem8  8107  ackbij1lem14  8113  ackbij1lem16  8115  ackbij2lem3  8121  cardcf  8132  sornom  8157  fin23lem28  8220  isf32lem2  8234  itunitc  8301  ituniiun  8302  axdc3lem2  8331  axdc4lem  8335  ttukeylem3  8391  ttukey2g  8396  fpwwe2lem8  8512  fpwwecbv  8519  canth4  8522  pwfseqlem2  8534  addcanpi  8776  mulcanpi  8777  recrecnq  8844  ltexnq  8852  genpv  8876  0idsr  8972  1idsr  8973  ax1rid  9036  mulid1  9088  addcan  9250  addcan2  9251  mulcand  9655  mulcan2d  9656  div11  9704  divmuleq  9719  conjmul  9731  eqneg  9734  ofsubeq0  9997  rpnnen1  10605  cnref1o  10607  xmulasslem  10864  xmulass  10866  xadddi2  10876  prunioo  11025  fzsuc2  11104  fzprval  11106  fztpval  11107  modadd1  11278  modmul1  11279  om2uzsuci  11288  om2uzrdg  11296  uzrdgxfr  11306  seq1  11336  seqp1  11338  seqfveq2  11345  seqfveq  11347  seqshft2  11349  seqsplit  11356  seqcaopr3  11358  seqcaopr2  11359  seqf1olem2a  11361  seqf1olem2  11363  seqf1o  11364  seqid  11368  seqid2  11369  seqhomo  11370  ser1const  11379  seqof2  11381  mulexp  11419  expadd  11422  expmul  11425  binom2  11496  sq01  11501  modexp  11514  bcpasc  11612  hashgadd  11651  hashdom  11653  hashfzo  11694  hashxplem  11696  hashxp  11697  hashmap  11698  hashpw  11699  hashbclem  11701  hashbc  11702  hashfacen  11703  hashf1lem1  11704  hashf1lem2  11705  hashf1  11706  seqcoll  11712  ccatopth  11776  ccatopth2  11777  cats1un  11790  replim  11921  cjreb  11928  cjexp  11955  absexp  12109  abs1m  12139  recan  12140  isercoll2  12462  iseraltlem2  12476  iseraltlem3  12477  sumeq2w  12486  sumeq2ii  12487  zsum  12512  fsum  12514  fsumf1o  12517  sumss  12518  fsumcvg2  12521  fsumadd  12532  isummulc2  12546  fsum2d  12555  fsummulc2  12567  fsumconst  12573  fsumparts  12585  fsumrelem  12586  fsumiun  12600  binom  12609  bcxmas  12615  incexclem  12616  isumshft  12619  isumnn0nn  12622  climcndslem1  12629  climcndslem2  12630  mertenslem2  12662  efne0  12698  efexp  12702  demoivreALT  12802  moddvds  12859  bitsinv1  12954  sadadd2  12972  smu01lem  12997  smupval  13000  smueqlem  13002  smumullem  13004  gcdaddm  13029  bezoutlem1  13038  bezout  13042  gcddiv  13049  seq1st  13062  alginv  13066  algfx  13071  isprm2lem  13086  nn0gcdsq  13144  crt  13167  eulerthlem2  13171  pythagtriplem1  13190  iserodd  13209  pcqmul  13227  pcexp  13233  pcneg  13247  pcmpt  13261  pcfac  13268  prmreclem2  13285  prmreclem3  13286  1arith  13295  vdwpc  13348  ramcl  13397  imasval  13737  ercpbllem  13773  xpscfv  13787  iscat  13897  iscatd  13898  catideu  13900  iscatd2  13906  catlid  13908  catrid  13909  catass  13911  proplem  13915  homfeq  13920  comfeq  13932  catpropd  13935  moni  13962  epii  13969  sectffval  13976  sectfval  13977  oppcsect  13999  sectmon  14003  isfunc  14061  funcid  14067  funcco  14068  funcpropd  14097  isfull  14107  fthsect  14122  fthmon  14124  natfval  14143  isnat  14144  nati  14152  fucsect  14169  natpropd  14173  setcmon  14242  setcepi  14243  setcsect  14244  evlfcl  14319  uncfcurf  14336  yoniso  14382  isacs5lem  14595  acsdrscl  14596  acsficl  14597  latdisdlem  14615  latdisd  14616  isdlat  14619  dlatmjdi  14620  isps  14634  ismnd  14692  mgmidmo  14693  mndlem1  14694  mgmlrid  14712  ismndd  14719  mndpropd  14721  imasmnd2  14732  ismhm  14740  mhmpropd  14744  mhmlin  14745  mhmeql  14764  gsumvalx  14774  gsumval2  14783  gsumccat  14787  gsumwmhm  14790  frmdgsum  14807  isgrp  14816  grppropd  14823  isgrpd2e  14827  isgrpid2  14841  grpidd2  14842  grpinvfval  14843  grpinvpropd  14866  grpsubrcan  14870  grplactcnv  14887  mulgnn0p1  14901  mulgneg2  14917  mulgnnass  14918  mulgnn0ass  14919  mulgass  14920  mhmmulg  14922  imasgrp2  14933  isghm  15006  ghmlin  15011  ghmeql  15028  isga  15068  gagrpid  15071  gaass  15074  galcan  15081  orbsta  15090  cayleylem2  15111  cntzfval  15119  elcntz  15121  cntzsnval  15123  elcntzsn  15124  cntzi  15128  resscntz  15130  cntzmhm  15137  gsumwrev  15162  odfval  15171  mndodcong  15180  odbezout  15194  odeq1  15196  submod  15203  gexval  15212  gexdvds  15218  ispgp  15226  sylow1lem1  15232  sylow2alem1  15251  sylow2alem2  15252  sylow2blem2  15255  efgmnvl  15346  efgredlemc  15377  efgredeu  15384  frgpuptinv  15403  frgpup1  15407  frgpup3lem  15409  iscmn  15419  cmnpropd  15421  iscmnd  15424  abladdsub4  15438  submcmn2  15458  divsabl  15480  iscyg  15489  cygabl  15500  gsum2d  15546  dmdprd  15559  dprdval  15561  dprdfcntz  15573  subgdmdprd  15592  dprd2da  15600  dpjrid  15620  pgpfac1lem3a  15634  ablfaclem3  15645  ablfac2  15647  isrng  15668  rngpropd  15695  mulgass2  15710  imasrng  15725  dvdsr  15751  dvreq1  15798  isdrng  15839  drngprop  15846  isdrngd  15860  drngpropd  15862  isabv  15907  abvmul  15917  issrng  15938  issrngd  15949  islmod  15954  lmodlema  15955  islmodd  15956  lmodprop2d  16006  islmhm  16103  lmhmlin  16111  islmhm2  16114  lmhmeql  16131  lmhmpropd  16145  islbs  16148  lbspropd  16171  divscrng  16311  islpir  16320  rrgval  16347  unitrrg  16353  isassa  16375  assalem  16376  isassad  16382  assapropd  16386  mvrf1  16489  mplmonmul  16527  mplcoe1  16528  mplcoe3  16529  mplcoe2  16530  coe1tm  16665  ply1sclf1  16680  cnfldmulg  16733  cnfldexp  16734  prmirredlem  16773  chrcong  16810  zndvds  16830  znf1o  16832  znunit  16844  cygznlem3  16850  frgpcyg  16854  isphl  16859  ipcj  16865  iporthcom  16866  ip2eq  16884  isphld  16885  phlpropd  16886  ocvfval  16893  iscss  16910  ishil  16945  isobs  16947  obsip  16948  obslbs  16957  isperf  17215  restperf  17248  cmpsub  17463  iscon  17476  2ndcsep  17522  elptr2  17606  ptbasin  17609  dfac14  17650  txcnp  17652  ptcnplem  17653  ptcnp  17654  cnmpt11  17695  cnmpt21  17703  cnmptcom  17710  kqfeq  17756  isr0  17769  pt1hmeo  17838  ustexsym  18245  isusp  18291  imasdsf1olem  18403  isxms  18477  xmspropd  18503  imasf1oxms  18519  stdbdmopn  18548  isngp3  18645  ngppropd  18678  isnlm  18711  nmvs  18712  xrsxmet  18840  cnheibor  18980  htpyi  18999  htpycc  19005  pi1xfr  19080  pi1coghm  19086  isclm  19089  lmhmclm  19111  clmmulg  19118  iscph  19133  tchcph  19194  cmetcaulem  19241  bcth3  19284  ovolunlem1a  19392  ovolicc2lem1  19413  ovolicc2lem4  19416  ovolicc2  19418  mblsplit  19428  volun  19439  volfiniun  19441  voliunlem1  19444  volsup  19450  ioorinv  19468  uniioombllem2  19475  vitalilem3  19502  mbfeqalem  19534  mbflim  19560  itgeqa  19705  itgconst  19710  itgfsum  19718  itgsplitioo  19729  dvnadd  19815  dvnres  19817  dvexp  19839  dvmptfsum  19859  mvth  19876  dvlip  19877  lhop1lem  19897  dvcvx  19904  evlslem1  19936  mpfrcl  19939  evlsval  19940  mdegle0  20000  ply1nzb  20045  mon1pval  20064  facth1  20087  ig1pval  20095  dgrmulc  20189  dgrcolem1  20191  dgrcolem2  20192  dgrco  20193  coecj  20196  vieta1lem2  20228  vieta1  20229  elqaalem3  20238  dvntaylp  20287  ulmss  20313  mtest  20320  sineq0  20429  efif1olem4  20447  cxpexp  20559  mulcxplem  20575  mulcxp  20576  cxpmul2  20580  cxpeq  20641  affineequiv2  20668  quad2  20679  dcubic  20686  leibpi  20782  o1cxp  20813  scvxcvx  20824  wilthlem1  20851  wilthlem2  20852  perfect  21015  dchrelbas2  21021  dchrinv  21045  dchrptlem2  21049  lgsne0  21117  lgsqrlem2  21126  lgsdchr  21132  lgseisenlem2  21134  lgsquad2lem2  21143  dchrisumlem1  21183  qabvexp  21320  ostthlem1  21321  ostthlem2  21322  ostth3  21332  usgraidx2v  21412  nbgraf1olem5  21455  cusgrasize  21487  wlkntrllem2  21560  2wlklem  21564  constr1trl  21588  redwlk  21606  wlkdvspthlem  21607  iscrct  21611  iscycl  21612  fargshiftf1  21624  fargshiftfva  21626  usgrcyclnl2  21628  3v3e3cycl1  21631  constr3trllem5  21641  4cycl4v4e  21653  4cycl4dv4e  21655  iseupa  21687  eupatrl  21690  eupaseg  21695  eupap1  21698  eupath2  21702  isgrpo  21784  grpoass  21791  grpoidinvlem3  21794  grpoidinv  21796  grpoideu  21797  grpoidinv2  21806  grpoinvfval  21812  isgrp2d  21823  gxcom  21857  gxinv  21858  gxnn0add  21862  gxnn0mul  21865  isablo  21871  ablocom  21873  gxdi  21884  issubgoilem  21897  isass  21904  opidon  21910  exidu1  21914  cmpidelt  21917  elghomlem2  21950  ghomlin  21952  ghgrplem2  21955  ghgrp  21956  ghablo  21957  isrngo  21966  rngoid  21971  rngoideu  21972  rngodi  21973  rngodir  21974  rngoass  21975  iscom2  22000  vci  22027  vcid  22030  vcdi  22031  vcdir  22032  vcass  22033  isvclem  22056  isnvlem  22089  nvmeq0  22145  nvs  22151  imsmetlem  22182  islno  22254  lnolin  22255  ishmo  22312  isphg  22318  phpar2  22324  phpar  22325  ipdiri  22331  ipasslem1  22332  ipasslem5  22336  ipasslem11  22341  ipassi  22342  dipdir  22343  dipass  22346  ip2eqi  22358  htth  22421  hvsubsub4  22562  hvnegdi  22569  hvaddcan  22572  hvaddcan2  22573  hvsubcan  22576  hvsubcan2  22577  hvaddsub4  22580  hial2eq  22608  normlem9at  22623  normsq  22636  norm-iii  22642  normsub  22645  normpyth  22647  normpar  22657  polid  22661  ococ  22908  chj0  22999  chlejb1  23014  chdmm1  23027  chjass  23035  spanun  23047  spansn  23061  elspansn2  23069  cmbr  23086  cmbr3  23110  pjoml2  23113  pjoml3  23114  osum  23147  spansnj  23149  pjch1  23172  pjadji  23187  pjaddi  23188  pjinormi  23189  pjsubi  23190  pjmuli  23191  pjcjt2  23194  pjch  23196  pjopyth  23222  pjpyth  23227  hoaddcom  23277  hoaddass  23285  hocsubdir  23288  hoaddid1  23294  ho0sub  23300  honegsub  23302  adjsym  23336  eigrei  23337  eigre  23338  eigposi  23339  eigorth  23341  ellnop  23361  elhmop  23376  ellnfn  23386  cnvadj  23395  lnopl  23417  unop  23418  hmop  23425  lnfnl  23434  adj1  23436  eleigvec  23460  hoddi  23493  lnopeq0lem2  23509  lnopunilem1  23513  lnopunilem2  23514  lnopunii  23515  elunop2  23516  lnophmi  23521  lnfnmul  23551  cnlnadjlem5  23574  branmfn  23608  bra11  23611  hmopidmchi  23654  hmopidmch  23656  hmopidmpj  23657  pjss2coi  23667  pjssmi  23668  pjssge0i  23669  pjidmco  23684  dfpjop  23685  elpjrn  23693  isst  23716  ishst  23717  hstel2  23722  stj  23738  mdbr  23797  mdi  23798  mdbr3  23800  dmdbr  23802  dmdmd  23803  dmdi  23805  dmdbr3  23808  mddmd2  23812  mdsl1i  23824  chjatom  23860  iuninc  24011  fmptcof2  24076  bcm1n  24151  xmulcand  24167  xrsmulgzz  24200  pstmxmet  24292  cnre2csqlem  24308  mndpluscn  24312  qqhval2  24366  esumfzf  24459  esumcvg  24476  ofcfeqd2  24484  ismeas  24553  isrnmeas  24554  measvun  24563  probun  24677  facgam  24850  subfacp1lem3  24868  subfacp1lem4  24869  subfacp1lem5  24870  subfacp1lem6  24871  subfacval2  24873  erdszelem9  24885  sconpht  24916  ptpcon  24920  cvmliftmolem1  24968  cvmliftmolem2  24969  cvmliftlem10  24981  cvmlift2  25003  cvmliftphtlem  25004  ghomgrpilem1  25096  relexpsucr  25130  relexpsucl  25132  relexpcnv  25133  relexpadd  25138  sqdivzi  25184  mulcan2g  25190  shftvalg  25208  clim2prod  25216  prodfrec  25223  prodeq2w  25238  prodeq2ii  25239  zprod  25263  fprod  25267  fprodf1o  25272  fprodser  25275  fprodmul  25284  fproddiv  25285  prodsn  25286  fprodabs  25297  fprodefsum  25298  fprodconst  25302  fprod2d  25305  iprodefisumlem  25317  binomfallfac  25357  faclimlem1  25362  fprb  25397  rdgprc  25422  dfrdg2  25423  dfpred3g  25450  preddowncl  25471  poseq  25528  soseq  25529  wfr3g  25537  wfrlem1  25538  wfrlem12  25549  wfrlem14  25551  wfrlem15  25552  wfr2  25555  elwlim  25574  frr3g  25581  frrlem1  25582  frrlem11  25594  sltval2  25611  sltres  25619  nofulllem5  25661  fvsingle  25765  fullfunfv  25792  brcgr  25839  brbtwn2  25844  colinearalglem1  25845  colinearalg  25849  ax5seglem1  25867  ax5seglem2  25868  ax5seglem8  25875  ax5seglem9  25876  axlowdimlem13  25893  axlowdimlem16  25896  axlowdim1  25898  axcontlem1  25903  axcontlem2  25904  axcontlem6  25908  axcontlem7  25909  axcontlem8  25910  lineelsb2  26082  bpolydif  26101  rankung  26107  ranksng  26108  rankpwg  26110  voliunnfl  26250  volsupnfl  26251  opnregcld  26333  cldregopn  26334  neibastop3  26391  cocanfo  26419  upixp  26431  sdclem2  26446  caushft  26467  ismtycnv  26511  ismtyima  26512  ismtybndlem  26515  ismtyres  26517  bfplem2  26532  bfp  26533  grpoeqdivid  26556  ghomco  26558  rngohomval  26580  isrngohom  26581  rngohomadd  26585  rngohommul  26586  iscringd  26609  crngocom  26611  crngohomfo  26616  dmncan2  26687  fnelfp  26736  ismrcd2  26753  ismrc  26755  dvdsrabdioph  26870  fphpdo  26878  rmxypairf1o  26974  monotoddzzfi  27005  monotoddzz  27006  oddcomabszz  27007  rmxdioph  27087  expdiophlem2  27093  dnnumch3  27122  aomclem8  27136  islssfg  27145  unxpwdom3  27233  gicabl  27240  pmtrfrn  27377  cntzsdrg  27487  idomodle  27489  fgraphxp  27507  hausgraph  27508  caofcan  27517  expgrowth  27529  fmuldfeq  27689  climmulf  27706  climexp  27707  climsuse  27710  climrecf  27711  stoweidlem30  27755  stoweidlem48  27773  wallispilem4  27793  wallispi2lem1  27796  wallispi2lem2  27797  csbafv12g  27977  csbaovg  28020  swdeq  28196  swrdccatin1  28205  swrdccat3blem  28218  2cshwmod  28257  usg2wlkeq  28304  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2pthlem1  28310  usgra2pth  28311  isrgra  28369  2pthfrgra  28401  bnj1385  29204  bnj66  29231  bnj106  29239  bnj155  29250  bnj222  29254  bnj540  29263  bnj591  29282  bnj594  29283  bnj611  29289  bnj893  29299  bnj1000  29312  bnj966  29315  bnj1112  29352  bnj1234  29382  bnj1253  29386  bnj1280  29389  bnj1326  29395  bnj1450  29419  bnj1463  29424  bnj1529  29439  lshpset  29776  lcvexchlem4  29835  lcvexchlem5  29836  lflset  29857  islfl  29858  lfli  29859  islfld  29860  eqlkr3  29899  isopos  29978  oposlem  29981  opcon3b  29994  cmtvalN  30009  omllaw  30041  cvlexchb2  30129  cvlatexchb2  30133  cvlsupr2  30141  4atlem9  30400  4atlem10a  30401  4atlem11a  30404  4atlem12a  30407  4at2  30411  pmapglb2N  30568  pmapglb2xN  30569  paddasslem17  30633  ispsubclN  30734  ispsubcl2N  30744  lhpmod2i2  30835  lhpmod6i1  30836  4atexlemex2  30868  4atex  30873  4atex2-0aOLDN  30875  4atex2-0cOLDN  30877  ldilval  30910  ltrnfset  30914  ltrnset  30915  isltrn  30916  ltrneq2  30945  trnfsetN  30952  trnsetN  30953  istrnN  30954  cdlemd5  30999  cdleme0moN  31022  cdleme0nex  31087  cdleme18d  31092  cdleme31so  31176  cdleme31fv  31187  cdlemg2jlemOLDN  31390  cdlemg2fvlem  31391  cdlemg2klem  31392  istendo  31557  tendovalco  31562  tendoeq2  31571  dicelvalN  31976  dihval  32030  dihcnv11  32073  dihmeetlem13N  32117  dihlspsnat  32131  dochn0nv  32173  dochkrshp4  32187  lpolsetN  32280  lpolsatN  32286  lpolpolsatN  32287  lcfl1lem  32289  lclkrlem2a  32305  lclkrlem2e  32309  lcfls1lem  32332  lclkrs2  32338  lcdfval  32386  lcdval  32387  mapdffval  32424  mapdfval  32425  mapd0  32463  mapdpglem30  32500  mapdhval  32522  mapdheq2  32527  hdmap1vallem  32596  hdmap1val  32597  hdmap1cbv  32601  hdmapval3N  32639  hdmap10  32641  hdmapeq0  32645  hdmap14lem12  32680  hdmap14lem13  32681  hgmapfval  32687  hgmapvs  32692  hgmapvv  32727  hlhilocv  32758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator