Theorem eqcomi 2197

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 2195	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 145	1 |- B = A

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  eqtr2i  2215  eqtr3i  2216  eqtr4i  2217  eqtr3id  2240  eqtr3di  2241  eqtr4di  2244  eqtr4id  2245  eqeltrri  2267  eleqtrri  2269  eqeltrrid  2281  eleqtrrdi  2287  abid2  2314  abid2f  2362  eqnetrri  2389  neeqtrri  2393  eqsstrri  3212  sseqtrri  3214  eqsstrrid  3226  sseqtrrdi  3228  difdif2ss  3416  inrab2  3432  dfopg  3802  opid  3822  eqbrtrri  4052  breqtrri  4056  breqtrrdi  4071  pwin  4313  limon  4545  tfis  4615  dfdm2  5200  cnvresid  5328  fores  5486  funcoeqres  5531  f1oprg  5544  fnmptfvd  5662  fmptpr  5750  fsnunres  5760  idref  5799  riotaprop  5897  fo1st  6210  fo2nd  6211  fnmpoovd  6268  ixpsnf1o  6790  phplem4  6911  snnen2og  6915  phplem4on  6923  pw1dc0el  6967  ss1o0el1o  6969  sbthlemi5  7020  eldju  7127  casefun  7144  omp1eomlem  7153  exmidfodomrlemim  7261  caucvgsrlembound  7854  ax0id  7938  1p1e2  9099  1e2m1  9101  2p1e3  9115  3p1e4  9117  4p1e5  9118  5p1e6  9119  6p1e7  9120  7p1e8  9121  8p1e9  9122  div4p1lem1div2  9236  0mnnnnn0  9272  zeo  9422  num0u  9458  numsucc  9487  decsucc  9488  1e0p1  9489  nummac  9492  decsubi  9510  decmul1  9511  decmul10add  9516  6p5lem  9517  10m1e9  9543  5t5e25  9550  6t6e36  9555  8t6e48  9566  decbin3  9589  infrenegsupex  9659  ige3m2fz  10115  fseq1p1m1  10160  fz0tp  10188  fz0to4untppr  10190  1fv  10205  fzo0to42pr  10287  fzosplitprm1  10301  fldiv4lem1div2uz2  10375  xnn0nnen  10508  expnegap0  10618  sq4e2t8  10708  3dec  10785  fihashen1  10870  pr0hash2ex  10886  imi  11044  infxrnegsupex  11406  zsumdc  11527  fsumadd  11549  hashrabrex  11624  ntrivcvgap  11691  fprodmul  11734  fproddivapf  11774  fprodmodd  11784  efsep  11834  3dvdsdec  12006  3dvds2dec  12007  flodddiv4  12075  lcmneg  12212  ennnfonelem1  12564  nninfdclemp1  12607  ndxid  12642  2strstr1g  12739  srgfcl  13469  isrhm  13654  issubrng  13695  rmodislmod  13847  cnfld0  14059  cnfld1  14060  cnfldplusf  14062  cnfldui  14077  toponrestid  14189  istpsi  14207  distopon  14255  distps  14259  discld  14304  txbas  14426  txdis  14445  txdis1cn  14446  txhmeo  14487  txswaphmeolem  14488  dvmptidcn  14863  sinq34lt0t  14966  loge  15002  2logb9irr  15103  2logb9irrALT  15106  sqrt2cxp2logb9e3  15107  2logb9irrap  15109  lgsdir  15151  2lgsoddprmlem3d  15198  2sqlem9  15211  2sqlem10  15212  ex-ceil  15218  ex-gcd  15223  bj-charfundcALT  15301  bdceqir  15336  bj-ssom  15428  trilpolemgt1  15529  redcwlpolemeq1  15544