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

Theorem eqeq12d 2451
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 2449 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653
This theorem is referenced by:  cdeqeq  3157  sbceqg  3268  csbing  3549  csbifg  3768  uniprg  4031  unisng  4033  intprg  4085  iununi  4176  csbopabg  4284  limeq  4594  ordunisuc  4813  onsucuni2  4815  orduninsuc  4824  csbima12g  5214  dmsnsnsn  5349  cnvsng  5356  csbiotag  5448  csbfv12gALT  5740  fveqres  5765  fvmptf  5822  eqfnfv2f  5832  fvreseq  5834  fmptco  5902  fnressn  5919  fvsng  5928  fnpr  5951  fnprOLD  5952  fnsuppres  5953  cocan1  6025  cocan2  6026  fliftfun  6035  weniso  6076  csbovg  6113  eqfnov  6177  ovmpt2s  6198  ov2gf  6199  ovmpt2dxf  6200  caovcomg  6243  caovassg  6246  caovcang  6249  caovcanrd  6251  caovcan  6252  caovdig  6262  caovdirg  6265  caovmo  6285  grprinvlem  6286  grprinvd  6287  offveqb  6327  caofid0l  6333  caofid0r  6334  caofass  6339  caonncan  6343  op1stg  6360  op2ndg  6361  f1o2ndf1  6455  opabiota  6539  csbriotag  6563  onfununi  6604  tfrlem1  6637  tfrlem2  6638  tfrlem3  6639  tfrlem3a  6640  tfrlem9  6647  tfrlem11  6650  tfrlem12  6651  tfr3  6661  tz7.44-1  6665  tz7.44-2  6666  tz7.44-3  6667  rdglem1  6674  rdg0g  6686  seqomlem1  6708  abianfp  6717  oalim  6777  omlim  6778  oelim  6779  oa0r  6783  om0r  6784  om1r  6787  oaass  6805  oarec  6806  odi  6823  omass  6824  oelim2  6839  oeoalem  6840  oeoa  6841  oeoelem  6842  oeoe  6843  nna0r  6853  nnacom  6861  nnaass  6866  nndi  6867  nnmass  6868  nnmsucr  6869  nnmcom  6870  oaabs  6888  oaabs2  6889  omabs  6891  ecovcom  7016  ecovass  7017  ecovdi  7018  dom2lem  7148  unxpdomlem2  7315  unxpdomlem3  7316  ixpfi2  7406  fipreima  7413  ordiso2  7485  wemaplem1  7516  wemaplem2  7517  wemapso2lem  7520  cantnfval2  7625  cantnfp1lem3  7637  oemapvali  7641  cantnflem1c  7644  cantnflem1  7646  wemapwe  7655  tcvalg  7678  rankvalg  7744  rankonidlem  7755  ranklim  7771  rankuni  7790  cardprclem  7867  cardprc  7868  carduni  7869  fseqenlem1  7906  fodomacn  7938  alephcard  7952  alephfp2  7991  alephval3  7992  dfac12lem1  8024  dfac12lem2  8025  dfac12r  8027  ackbij1lem5  8105  ackbij1lem8  8108  ackbij1lem14  8114  ackbij1lem16  8116  ackbij2lem3  8122  cardcf  8133  sornom  8158  fin23lem28  8221  isf32lem2  8235  itunitc  8302  ituniiun  8303  axdc3lem2  8332  axdc4lem  8336  ttukeylem3  8392  ttukey2g  8397  fpwwe2lem8  8513  fpwwecbv  8520  canth4  8523  pwfseqlem2  8535  addcanpi  8777  mulcanpi  8778  recrecnq  8845  ltexnq  8853  genpv  8877  0idsr  8973  1idsr  8974  ax1rid  9037  mulid1  9089  addcan  9251  addcan2  9252  mulcand  9656  mulcan2d  9657  div11  9705  divmuleq  9720  conjmul  9732  eqneg  9735  ofsubeq0  9998  rpnnen1  10606  cnref1o  10608  xmulasslem  10865  xmulass  10867  xadddi2  10877  prunioo  11026  fzsuc2  11105  fzprval  11107  fztpval  11108  modadd1  11279  modmul1  11280  om2uzsuci  11289  om2uzrdg  11297  uzrdgxfr  11307  seq1  11337  seqp1  11339  seqfveq2  11346  seqfveq  11348  seqshft2  11350  seqsplit  11357  seqcaopr3  11359  seqcaopr2  11360  seqf1olem2a  11362  seqf1olem2  11364  seqf1o  11365  seqid  11369  seqid2  11370  seqhomo  11371  ser1const  11380  seqof2  11382  mulexp  11420  expadd  11423  expmul  11426  binom2  11497  sq01  11502  modexp  11515  bcpasc  11613  hashgadd  11652  hashdom  11654  hashfzo  11695  hashxplem  11697  hashxp  11698  hashmap  11699  hashpw  11700  hashbclem  11702  hashbc  11703  hashfacen  11704  hashf1lem1  11705  hashf1lem2  11706  hashf1  11707  seqcoll  11713  ccatopth  11777  ccatopth2  11778  cats1un  11791  replim  11922  cjreb  11929  cjexp  11956  absexp  12110  abs1m  12140  recan  12141  isercoll2  12463  iseraltlem2  12477  iseraltlem3  12478  sumeq2w  12487  sumeq2ii  12488  zsum  12513  fsum  12515  fsumf1o  12518  sumss  12519  fsumcvg2  12522  fsumadd  12533  isummulc2  12547  fsum2d  12556  fsummulc2  12568  fsumconst  12574  fsumparts  12586  fsumrelem  12587  fsumiun  12601  binom  12610  bcxmas  12616  incexclem  12617  isumshft  12620  isumnn0nn  12623  climcndslem1  12630  climcndslem2  12631  mertenslem2  12663  efne0  12699  efexp  12703  demoivreALT  12803  moddvds  12860  bitsinv1  12955  sadadd2  12973  smu01lem  12998  smupval  13001  smueqlem  13003  smumullem  13005  gcdaddm  13030  bezoutlem1  13039  bezout  13043  gcddiv  13050  seq1st  13063  alginv  13067  algfx  13072  isprm2lem  13087  nn0gcdsq  13145  crt  13168  eulerthlem2  13172  pythagtriplem1  13191  iserodd  13210  pcqmul  13228  pcexp  13234  pcneg  13248  pcmpt  13262  pcfac  13269  prmreclem2  13286  prmreclem3  13287  1arith  13296  vdwpc  13349  ramcl  13398  imasval  13738  ercpbllem  13774  xpscfv  13788  iscat  13898  iscatd  13899  catideu  13901  iscatd2  13907  catlid  13909  catrid  13910  catass  13912  proplem  13916  homfeq  13921  comfeq  13933  catpropd  13936  moni  13963  epii  13970  sectffval  13977  sectfval  13978  oppcsect  14000  sectmon  14004  isfunc  14062  funcid  14068  funcco  14069  funcpropd  14098  isfull  14108  fthsect  14123  fthmon  14125  natfval  14144  isnat  14145  nati  14153  fucsect  14170  natpropd  14174  setcmon  14243  setcepi  14244  setcsect  14245  evlfcl  14320  uncfcurf  14337  yoniso  14383  isacs5lem  14596  acsdrscl  14597  acsficl  14598  latdisdlem  14616  latdisd  14617  isdlat  14620  dlatmjdi  14621  isps  14635  ismnd  14693  mgmidmo  14694  mndlem1  14695  mgmlrid  14713  ismndd  14720  mndpropd  14722  imasmnd2  14733  ismhm  14741  mhmpropd  14745  mhmlin  14746  mhmeql  14765  gsumvalx  14775  gsumval2  14784  gsumccat  14788  gsumwmhm  14791  frmdgsum  14808  isgrp  14817  grppropd  14824  isgrpd2e  14828  isgrpid2  14842  grpidd2  14843  grpinvfval  14844  grpinvpropd  14867  grpsubrcan  14871  grplactcnv  14888  mulgnn0p1  14902  mulgneg2  14918  mulgnnass  14919  mulgnn0ass  14920  mulgass  14921  mhmmulg  14923  imasgrp2  14934  isghm  15007  ghmlin  15012  ghmeql  15029  isga  15069  gagrpid  15072  gaass  15075  galcan  15082  orbsta  15091  cayleylem2  15112  cntzfval  15120  elcntz  15122  cntzsnval  15124  elcntzsn  15125  cntzi  15129  resscntz  15131  cntzmhm  15138  gsumwrev  15163  odfval  15172  mndodcong  15181  odbezout  15195  odeq1  15197  submod  15204  gexval  15213  gexdvds  15219  ispgp  15227  sylow1lem1  15233  sylow2alem1  15252  sylow2alem2  15253  sylow2blem2  15256  efgmnvl  15347  efgredlemc  15378  efgredeu  15385  frgpuptinv  15404  frgpup1  15408  frgpup3lem  15410  iscmn  15420  cmnpropd  15422  iscmnd  15425  abladdsub4  15439  submcmn2  15459  divsabl  15481  iscyg  15490  cygabl  15501  gsum2d  15547  dmdprd  15560  dprdval  15562  dprdfcntz  15574  subgdmdprd  15593  dprd2da  15601  dpjrid  15621  pgpfac1lem3a  15635  ablfaclem3  15646  ablfac2  15648  isrng  15669  rngpropd  15696  mulgass2  15711  imasrng  15726  dvdsr  15752  dvreq1  15799  isdrng  15840  drngprop  15847  isdrngd  15861  drngpropd  15863  isabv  15908  abvmul  15918  issrng  15939  issrngd  15950  islmod  15955  lmodlema  15956  islmodd  15957  lmodprop2d  16007  islmhm  16104  lmhmlin  16112  islmhm2  16115  lmhmeql  16132  lmhmpropd  16146  islbs  16149  lbspropd  16172  divscrng  16312  islpir  16321  rrgval  16348  unitrrg  16354  isassa  16376  assalem  16377  isassad  16383  assapropd  16387  mvrf1  16490  mplmonmul  16528  mplcoe1  16529  mplcoe3  16530  mplcoe2  16531  coe1tm  16666  ply1sclf1  16681  cnfldmulg  16734  cnfldexp  16735  prmirredlem  16774  chrcong  16811  zndvds  16831  znf1o  16833  znunit  16845  cygznlem3  16851  frgpcyg  16855  isphl  16860  ipcj  16866  iporthcom  16867  ip2eq  16885  isphld  16886  phlpropd  16887  ocvfval  16894  iscss  16911  ishil  16946  isobs  16948  obsip  16949  obslbs  16958  isperf  17216  restperf  17249  cmpsub  17464  iscon  17477  2ndcsep  17523  elptr2  17607  ptbasin  17610  dfac14  17651  txcnp  17653  ptcnplem  17654  ptcnp  17655  cnmpt11  17696  cnmpt21  17704  cnmptcom  17711  kqfeq  17757  isr0  17770  pt1hmeo  17839  ustexsym  18246  isusp  18292  imasdsf1olem  18404  isxms  18478  xmspropd  18504  imasf1oxms  18520  stdbdmopn  18549  isngp3  18646  ngppropd  18679  isnlm  18712  nmvs  18713  xrsxmet  18841  cnheibor  18981  htpyi  19000  htpycc  19006  pi1xfr  19081  pi1coghm  19087  isclm  19090  lmhmclm  19112  clmmulg  19119  iscph  19134  tchcph  19195  cmetcaulem  19242  bcth3  19285  ovolunlem1a  19393  ovolicc2lem1  19414  ovolicc2lem4  19417  ovolicc2  19419  mblsplit  19429  volun  19440  volfiniun  19442  voliunlem1  19445  volsup  19451  ioorinv  19469  uniioombllem2  19476  vitalilem3  19503  mbfeqalem  19535  mbflim  19561  itgeqa  19706  itgconst  19711  itgfsum  19719  itgsplitioo  19730  dvnadd  19816  dvnres  19818  dvexp  19840  dvmptfsum  19860  mvth  19877  dvlip  19878  lhop1lem  19898  dvcvx  19905  evlslem1  19937  mpfrcl  19940  evlsval  19941  mdegle0  20001  ply1nzb  20046  mon1pval  20065  facth1  20088  ig1pval  20096  dgrmulc  20190  dgrcolem1  20192  dgrcolem2  20193  dgrco  20194  coecj  20197  vieta1lem2  20229  vieta1  20230  elqaalem3  20239  dvntaylp  20288  ulmss  20314  mtest  20321  sineq0  20430  efif1olem4  20448  cxpexp  20560  mulcxplem  20576  mulcxp  20577  cxpmul2  20581  cxpeq  20642  affineequiv2  20669  quad2  20680  dcubic  20687  leibpi  20783  o1cxp  20814  scvxcvx  20825  wilthlem1  20852  wilthlem2  20853  perfect  21016  dchrelbas2  21022  dchrinv  21046  dchrptlem2  21050  lgsne0  21118  lgsqrlem2  21127  lgsdchr  21133  lgseisenlem2  21135  lgsquad2lem2  21144  dchrisumlem1  21184  qabvexp  21321  ostthlem1  21322  ostthlem2  21323  ostth3  21333  usgraidx2v  21413  nbgraf1olem5  21456  cusgrasize  21488  wlkntrllem2  21561  2wlklem  21565  constr1trl  21589  redwlk  21607  wlkdvspthlem  21608  iscrct  21612  iscycl  21613  fargshiftf1  21625  fargshiftfva  21627  usgrcyclnl2  21629  3v3e3cycl1  21632  constr3trllem5  21642  4cycl4v4e  21654  4cycl4dv4e  21656  iseupa  21688  eupatrl  21691  eupaseg  21696  eupap1  21699  eupath2  21703  isgrpo  21785  grpoass  21792  grpoidinvlem3  21795  grpoidinv  21797  grpoideu  21798  grpoidinv2  21807  grpoinvfval  21813  isgrp2d  21824  gxcom  21858  gxinv  21859  gxnn0add  21863  gxnn0mul  21866  isablo  21872  ablocom  21874  gxdi  21885  issubgoilem  21898  isass  21905  opidon  21911  exidu1  21915  cmpidelt  21918  elghomlem2  21951  ghomlin  21953  ghgrplem2  21956  ghgrp  21957  ghablo  21958  isrngo  21967  rngoid  21972  rngoideu  21973  rngodi  21974  rngodir  21975  rngoass  21976  iscom2  22001  vci  22028  vcid  22031  vcdi  22032  vcdir  22033  vcass  22034  isvclem  22057  isnvlem  22090  nvmeq0  22146  nvs  22152  imsmetlem  22183  islno  22255  lnolin  22256  ishmo  22313  isphg  22319  phpar2  22325  phpar  22326  ipdiri  22332  ipasslem1  22333  ipasslem5  22337  ipasslem11  22342  ipassi  22343  dipdir  22344  dipass  22347  ip2eqi  22359  htth  22422  hvsubsub4  22563  hvnegdi  22570  hvaddcan  22573  hvaddcan2  22574  hvsubcan  22577  hvsubcan2  22578  hvaddsub4  22581  hial2eq  22609  normlem9at  22624  normsq  22637  norm-iii  22643  normsub  22646  normpyth  22648  normpar  22658  polid  22662  ococ  22909  chj0  23000  chlejb1  23015  chdmm1  23028  chjass  23036  spanun  23048  spansn  23062  elspansn2  23070  cmbr  23087  cmbr3  23111  pjoml2  23114  pjoml3  23115  osum  23148  spansnj  23150  pjch1  23173  pjadji  23188  pjaddi  23189  pjinormi  23190  pjsubi  23191  pjmuli  23192  pjcjt2  23195  pjch  23197  pjopyth  23223  pjpyth  23228  hoaddcom  23278  hoaddass  23286  hocsubdir  23289  hoaddid1  23295  ho0sub  23301  honegsub  23303  adjsym  23337  eigrei  23338  eigre  23339  eigposi  23340  eigorth  23342  ellnop  23362  elhmop  23377  ellnfn  23387  cnvadj  23396  lnopl  23418  unop  23419  hmop  23426  lnfnl  23435  adj1  23437  eleigvec  23461  hoddi  23494  lnopeq0lem2  23510  lnopunilem1  23514  lnopunilem2  23515  lnopunii  23516  elunop2  23517  lnophmi  23522  lnfnmul  23552  cnlnadjlem5  23575  branmfn  23609  bra11  23612  hmopidmchi  23655  hmopidmch  23657  hmopidmpj  23658  pjss2coi  23668  pjssmi  23669  pjssge0i  23670  pjidmco  23685  dfpjop  23686  elpjrn  23694  isst  23717  ishst  23718  hstel2  23723  stj  23739  mdbr  23798  mdi  23799  mdbr3  23801  dmdbr  23803  dmdmd  23804  dmdi  23806  dmdbr3  23809  mddmd2  23813  mdsl1i  23825  chjatom  23861  iuninc  24012  fmptcof2  24077  bcm1n  24152  xmulcand  24168  xrsmulgzz  24201  pstmxmet  24293  cnre2csqlem  24309  mndpluscn  24313  qqhval2  24367  esumfzf  24460  esumcvg  24477  ofcfeqd2  24485  ismeas  24554  isrnmeas  24555  measvun  24564  probun  24678  facgam  24851  subfacp1lem3  24869  subfacp1lem4  24870  subfacp1lem5  24871  subfacp1lem6  24872  subfacval2  24874  erdszelem9  24886  sconpht  24917  ptpcon  24921  cvmliftmolem1  24969  cvmliftmolem2  24970  cvmliftlem10  24982  cvmlift2  25004  cvmliftphtlem  25005  ghomgrpilem1  25097  relexpsucr  25131  relexpsucl  25133  relexpcnv  25134  relexpadd  25139  sqdivzi  25185  mulcan2g  25191  shftvalg  25209  clim2prod  25217  prodfrec  25224  prodeq2w  25239  prodeq2ii  25240  zprod  25264  fprod  25268  fprodf1o  25273  fprodser  25276  fprodmul  25285  fproddiv  25286  prodsn  25287  fprodabs  25298  fprodefsum  25299  fprodconst  25303  fprod2d  25306  iprodefisumlem  25318  binomfallfac  25358  faclimlem1  25363  fprb  25398  rdgprc  25423  dfrdg2  25424  dfpred3g  25451  preddowncl  25472  poseq  25529  soseq  25530  wfr3g  25538  wfrlem1  25539  wfrlem12  25550  wfrlem14  25552  wfrlem15  25553  wfr2  25556  elwlim  25575  frr3g  25582  frrlem1  25583  frrlem11  25595  sltval2  25612  sltres  25620  nofulllem5  25662  fvsingle  25766  fullfunfv  25793  brcgr  25840  brbtwn2  25845  colinearalglem1  25846  colinearalg  25850  ax5seglem1  25868  ax5seglem2  25869  ax5seglem8  25876  ax5seglem9  25877  axlowdimlem13  25894  axlowdimlem16  25897  axlowdim1  25899  axcontlem1  25904  axcontlem2  25905  axcontlem6  25909  axcontlem7  25910  axcontlem8  25911  lineelsb2  26083  bpolydif  26102  rankung  26108  ranksng  26109  rankpwg  26111  voliunnfl  26251  volsupnfl  26252  opnregcld  26334  cldregopn  26335  neibastop3  26392  cocanfo  26420  upixp  26432  sdclem2  26447  caushft  26468  ismtycnv  26512  ismtyima  26513  ismtybndlem  26516  ismtyres  26518  bfplem2  26533  bfp  26534  grpoeqdivid  26557  ghomco  26559  rngohomval  26581  isrngohom  26582  rngohomadd  26586  rngohommul  26587  iscringd  26610  crngocom  26612  crngohomfo  26617  dmncan2  26688  fnelfp  26737  ismrcd2  26754  ismrc  26756  dvdsrabdioph  26871  fphpdo  26879  rmxypairf1o  26975  monotoddzzfi  27006  monotoddzz  27007  oddcomabszz  27008  rmxdioph  27088  expdiophlem2  27094  dnnumch3  27123  aomclem8  27137  islssfg  27146  unxpwdom3  27234  gicabl  27241  pmtrfrn  27378  cntzsdrg  27488  idomodle  27490  fgraphxp  27508  hausgraph  27509  caofcan  27518  expgrowth  27530  fmuldfeq  27690  climmulf  27707  climexp  27708  climsuse  27711  climrecf  27712  stoweidlem30  27756  stoweidlem48  27774  wallispilem4  27794  wallispi2lem1  27797  wallispi2lem2  27798  csbafv12g  27978  csbaovg  28021  swdeq  28197  swrdccatin1  28206  swrdccat3blem  28219  2cshwmod  28258  usg2wlkeq  28305  usgra2pthspth  28306  usgra2wlkspthlem1  28307  usgra2pthlem1  28311  usgra2pth  28312  isrgra  28370  2pthfrgra  28402  bnj1385  29205  bnj66  29232  bnj106  29240  bnj155  29251  bnj222  29255  bnj540  29264  bnj591  29283  bnj594  29284  bnj611  29290  bnj893  29300  bnj1000  29313  bnj966  29316  bnj1112  29353  bnj1234  29383  bnj1253  29387  bnj1280  29390  bnj1326  29396  bnj1450  29420  bnj1463  29425  bnj1529  29440  lshpset  29777  lcvexchlem4  29836  lcvexchlem5  29837  lflset  29858  islfl  29859  lfli  29860  islfld  29861  eqlkr3  29900  isopos  29979  oposlem  29982  opcon3b  29995  cmtvalN  30010  omllaw  30042  cvlexchb2  30130  cvlatexchb2  30134  cvlsupr2  30142  4atlem9  30401  4atlem10a  30402  4atlem11a  30405  4atlem12a  30408  4at2  30412  pmapglb2N  30569  pmapglb2xN  30570  paddasslem17  30634  ispsubclN  30735  ispsubcl2N  30745  lhpmod2i2  30836  lhpmod6i1  30837  4atexlemex2  30869  4atex  30874  4atex2-0aOLDN  30876  4atex2-0cOLDN  30878  ldilval  30911  ltrnfset  30915  ltrnset  30916  isltrn  30917  ltrneq2  30946  trnfsetN  30953  trnsetN  30954  istrnN  30955  cdlemd5  31000  cdleme0moN  31023  cdleme0nex  31088  cdleme18d  31093  cdleme31so  31177  cdleme31fv  31188  cdlemg2jlemOLDN  31391  cdlemg2fvlem  31392  cdlemg2klem  31393  istendo  31558  tendovalco  31563  tendoeq2  31572  dicelvalN  31977  dihval  32031  dihcnv11  32074  dihmeetlem13N  32118  dihlspsnat  32132  dochn0nv  32174  dochkrshp4  32188  lpolsetN  32281  lpolsatN  32287  lpolpolsatN  32288  lcfl1lem  32290  lclkrlem2a  32306  lclkrlem2e  32310  lcfls1lem  32333  lclkrs2  32339  lcdfval  32387  lcdval  32388  mapdffval  32425  mapdfval  32426  mapd0  32464  mapdpglem30  32501  mapdhval  32523  mapdheq2  32528  hdmap1vallem  32597  hdmap1val  32598  hdmap1cbv  32602  hdmapval3N  32640  hdmap10  32642  hdmapeq0  32646  hdmap14lem12  32681  hdmap14lem13  32682  hgmapfval  32688  hgmapvs  32693  hgmapvv  32728  hlhilocv  32759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2430
  Copyright terms: Public domain W3C validator