Theorem eqcomi 2233

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	|- A = B

Assertion

Ref	Expression
eqcomi	|- B = A

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 |- A = B
2		eqcom 2231	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 145	1 |- B = A

Syntax hints:   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  eqtr3id  2276  eqtr3di  2277  eqtr4di  2280  eqtr4id  2281  eqeltrri  2303  eleqtrri  2305  eqeltrrid  2317  eleqtrrdi  2323  abid2  2350  abid2f  2398  eqnetrri  2425  neeqtrri  2429  eqsstrri  3258  sseqtrri  3260  eqsstrrid  3272  sseqtrrdi  3274  difdif2ss  3462  inrab2  3478  dfopg  3858  opid  3878  eqbrtrri  4109  breqtrri  4113  breqtrrdi  4128  opwo0id  4339  pwin  4377  limon  4609  tfis  4679  dfdm2  5269  cnvresid  5401  fores  5566  funcoeqres  5611  f1oprg  5625  fvmbr  5670  fnmptfvd  5747  funopdmsn  5829  fmptpr  5841  fsnunres  5851  idref  5892  riotaeqimp  5991  riotaprop  5992  fo1st  6315  fo2nd  6316  fnmpoovd  6375  ixpsnf1o  6900  phplem4  7036  snnen2og  7040  phplem4on  7049  pw1dc0el  7096  ss1o0el1o  7098  sbthlemi5  7151  eldju  7258  casefun  7275  omp1eomlem  7284  exmidfodomrlemim  7402  caucvgsrlembound  8004  ax0id  8088  1p1e2  9250  1e2m1  9252  2p1e3  9267  3p1e4  9269  4p1e5  9270  5p1e6  9271  6p1e7  9272  7p1e8  9273  8p1e9  9274  div4p1lem1div2  9388  0mnnnnn0  9424  zeo  9575  num0u  9611  numsucc  9640  decsucc  9641  1e0p1  9642  nummac  9645  decsubi  9663  decmul1  9664  decmul10add  9669  6p5lem  9670  10m1e9  9696  5t5e25  9703  6t6e36  9708  8t6e48  9719  decbin3  9742  infrenegsupex  9818  ige3m2fz  10274  fseq1p1m1  10319  fz0tp  10347  fz0to4untppr  10349  1fv  10364  fzo0to42pr  10455  fzosplitpr  10469  fzosplitprm1  10470  fldiv4lem1div2uz2  10556  xnn0nnen  10689  expnegap0  10799  sq4e2t8  10889  3dec  10966  fihashen1  11051  pr0hash2ex  11069  fundm2domnop0  11099  pfxccat3  11305  swrdccat  11306  pfxccatpfx2  11308  swrdccat3blem  11310  swrdccat3b  11311  cats2catd  11340  imi  11451  infxrnegsupex  11814  zsumdc  11935  fsumadd  11957  hashrabrex  12032  ntrivcvgap  12099  fprodmul  12142  fproddivapf  12182  fprodmodd  12192  efsep  12242  3dvds  12415  3dvdsdec  12416  3dvds2dec  12417  flodddiv4  12487  lcmneg  12636  dec2dvds  12974  2exp5  12995  2exp11  12999  ennnfonelem1  13018  nninfdclemp1  13061  ndxid  13096  2strstr1g  13195  srgfcl  13976  isrhm  14162  issubrng  14203  rmodislmod  14355  cnfld0  14575  cnfld1  14576  cnfldplusf  14578  cnfldui  14593  toponrestid  14735  istpsi  14753  distopon  14801  distps  14805  discld  14850  txbas  14972  txdis  14991  txdis1cn  14992  txhmeo  15033  txswaphmeolem  15034  dvmptidcn  15428  dvmptid  15430  sinq34lt0t  15545  loge  15581  2logb9irr  15685  2logb9irrALT  15688  sqrt2cxp2logb9e3  15689  2logb9irrap  15691  lgsdir  15754  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3d1  15819  2lgsoddprmlem3d  15829  2sqlem9  15843  2sqlem10  15844  setsvtx  15892  edgiedgbg  15906  edg0iedg0g  15907  isuhgrm  15912  isushgrm  15913  uhgr0  15926  isupgren  15936  isumgren  15946  umgrpredgv  15986  isuspgren  15996  isusgren  15997  ausgrusgrben  16007  usgrf1oedg  16044  uhgr2edg  16045  usgredg3  16053  ushgredgedg  16065  ushgredgedgloop  16067  usgr0  16078  vtxdfifiun  16103  edginwlkd  16152  wlk1walkdom  16156  clwwlknon2x  16230  clwwlknonex2lem1  16232  ex-ceil  16258  ex-gcd  16263  bj-charfundcALT  16340  bdceqir  16375  bj-ssom  16467  trilpolemgt1  16579  redcwlpolemeq1  16594