Theorem eqcomi 2211

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2189

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

This theorem is referenced by:  eqtr2i  2229  eqtr3i  2230  eqtr4i  2231  eqtr3id  2254  eqtr3di  2255  eqtr4di  2258  eqtr4id  2259  eqeltrri  2281  eleqtrri  2283  eqeltrrid  2295  eleqtrrdi  2301  abid2  2328  abid2f  2376  eqnetrri  2403  neeqtrri  2407  eqsstrri  3234  sseqtrri  3236  eqsstrrid  3248  sseqtrrdi  3250  difdif2ss  3438  inrab2  3454  dfopg  3831  opid  3851  eqbrtrri  4082  breqtrri  4086  breqtrrdi  4101  opwo0id  4311  pwin  4347  limon  4579  tfis  4649  dfdm2  5236  cnvresid  5367  fores  5530  funcoeqres  5575  f1oprg  5589  fnmptfvd  5707  funopdmsn  5787  fmptpr  5799  fsnunres  5809  idref  5848  riotaprop  5946  fo1st  6266  fo2nd  6267  fnmpoovd  6324  ixpsnf1o  6846  phplem4  6977  snnen2og  6981  phplem4on  6990  pw1dc0el  7034  ss1o0el1o  7036  sbthlemi5  7089  eldju  7196  casefun  7213  omp1eomlem  7222  exmidfodomrlemim  7340  caucvgsrlembound  7942  ax0id  8026  1p1e2  9188  1e2m1  9190  2p1e3  9205  3p1e4  9207  4p1e5  9208  5p1e6  9209  6p1e7  9210  7p1e8  9211  8p1e9  9212  div4p1lem1div2  9326  0mnnnnn0  9362  zeo  9513  num0u  9549  numsucc  9578  decsucc  9579  1e0p1  9580  nummac  9583  decsubi  9601  decmul1  9602  decmul10add  9607  6p5lem  9608  10m1e9  9634  5t5e25  9641  6t6e36  9646  8t6e48  9657  decbin3  9680  infrenegsupex  9750  ige3m2fz  10206  fseq1p1m1  10251  fz0tp  10279  fz0to4untppr  10281  1fv  10296  fzo0to42pr  10386  fzosplitprm1  10400  fldiv4lem1div2uz2  10486  xnn0nnen  10619  expnegap0  10729  sq4e2t8  10819  3dec  10896  fihashen1  10981  pr0hash2ex  10997  fundm2domnop0  11027  pfxccat3  11225  swrdccat  11226  pfxccatpfx2  11228  swrdccat3blem  11230  swrdccat3b  11231  imi  11326  infxrnegsupex  11689  zsumdc  11810  fsumadd  11832  hashrabrex  11907  ntrivcvgap  11974  fprodmul  12017  fproddivapf  12057  fprodmodd  12067  efsep  12117  3dvds  12290  3dvdsdec  12291  3dvds2dec  12292  flodddiv4  12362  lcmneg  12511  dec2dvds  12849  2exp5  12870  2exp11  12874  ennnfonelem1  12893  nninfdclemp1  12936  ndxid  12971  2strstr1g  13069  srgfcl  13850  isrhm  14035  issubrng  14076  rmodislmod  14228  cnfld0  14448  cnfld1  14449  cnfldplusf  14451  cnfldui  14466  toponrestid  14608  istpsi  14626  distopon  14674  distps  14678  discld  14723  txbas  14845  txdis  14864  txdis1cn  14865  txhmeo  14906  txswaphmeolem  14907  dvmptidcn  15301  dvmptid  15303  sinq34lt0t  15418  loge  15454  2logb9irr  15558  2logb9irrALT  15561  sqrt2cxp2logb9e3  15562  2logb9irrap  15564  lgsdir  15627  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3d1  15692  2lgsoddprmlem3d  15702  2sqlem9  15716  2sqlem10  15717  edgiedgbg  15776  edg0iedg0g  15777  isuhgrm  15782  isushgrm  15783  uhgr0  15796  isupgren  15806  isumgren  15816  umgrpredgv  15851  ex-ceil  15862  ex-gcd  15867  bj-charfundcALT  15944  bdceqir  15979  bj-ssom  16071  trilpolemgt1  16180  redcwlpolemeq1  16195