Theorem eqcomi 2236

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  eqtr2i  2254  eqtr3i  2255  eqtr4i  2256  eqtr3id  2279  eqtr3di  2280  eqtr4di  2283  eqtr4id  2284  eqeltrri  2306  eleqtrri  2308  eqeltrrid  2320  eleqtrrdi  2326  abid2  2355  abid2f  2410  eqnetrri  2437  neeqtrri  2441  eqsstrri  3271  sseqtrri  3273  eqsstrrid  3285  sseqtrrdi  3287  difdif2ss  3478  inrab2  3494  dfopg  3881  opid  3901  eqbrtrri  4132  breqtrri  4136  breqtrrdi  4151  opwo0id  4365  pwin  4403  limon  4635  tfis  4705  dfdm2  5297  cnvresid  5430  fores  5600  funcoeqres  5645  f1oprg  5660  fvmbr  5705  fnmptfvd  5782  funopdmsn  5864  fmptpr  5876  fsnunres  5886  idref  5929  riotaeqimp  6028  riotaprop  6029  fo1st  6351  fo2nd  6352  fnmpoovd  6411  ixpsnf1o  6971  phplem4  7109  snnen2og  7113  phplem4on  7122  pw1dc0el  7171  ss1o0el1o  7173  sbthlemi5  7231  eldju  7359  casefun  7376  omp1eomlem  7385  exmidfodomrlemim  7504  caucvgsrlembound  8109  ax0id  8193  1p1e2  9354  1e2m1  9356  2p1e3  9371  3p1e4  9373  4p1e5  9374  5p1e6  9375  6p1e7  9376  7p1e8  9377  8p1e9  9378  div4p1lem1div2  9492  0mnnnnn0  9528  zeo  9683  num0u  9719  numsucc  9748  decsucc  9749  1e0p1  9750  nummac  9753  decsubi  9771  decmul1  9772  decmul10add  9777  6p5lem  9778  10m1e9  9804  5t5e25  9811  6t6e36  9816  8t6e48  9827  decbin3  9850  infrenegsupex  9926  ige3m2fz  10383  fseq1p1m1  10428  fz0tp  10456  fz0to4untppr  10458  1fv  10473  fzo0to42pr  10565  fzosplitpr  10579  fzosplitprm1  10580  fldiv4lem1div2uz2  10666  xnn0nnen  10799  expnegap0  10909  sq4e2t8  10999  3dec  11076  fihashen1  11162  pr0hash2ex  11180  fundm2domnop0  11220  pfxccat3  11426  swrdccat  11427  pfxccatpfx2  11429  swrdccat3blem  11431  swrdccat3b  11432  cats2catd  11461  imi  11585  infxrnegsupex  11948  zsumdc  12070  fsumadd  12092  hashrabrex  12167  ntrivcvgap  12234  fprodmul  12277  fproddivapf  12317  fprodmodd  12327  efsep  12377  3dvds  12550  3dvdsdec  12551  3dvds2dec  12552  flodddiv4  12622  lcmneg  12771  dec2dvds  13109  2exp5  13130  2exp11  13134  ennnfonelem1  13158  nninfdclemp1  13201  ndxid  13236  2strstr1g  13335  srgfcl  14117  isrhm  14303  issubrng  14344  rmodislmod  14499  cnfld0  14719  cnfld1  14720  cnfldplusf  14722  cnfldui  14737  toponrestid  14886  istpsi  14904  distopon  14952  distps  14956  discld  15001  txbas  15123  txdis  15142  txdis1cn  15143  txhmeo  15184  txswaphmeolem  15185  dvmptidcn  15579  dvmptid  15581  sinq34lt0t  15696  loge  15732  2logb9irr  15836  2logb9irrALT  15839  sqrt2cxp2logb9e3  15840  2logb9irrap  15842  lgsdir  15908  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3d1  15973  2lgsoddprmlem3d  15983  2sqlem9  15997  2sqlem10  15998  setsvtx  16046  edgiedgbg  16060  edg0iedg0g  16061  isuhgrm  16066  isushgrm  16067  uhgr0  16080  isupgren  16090  isumgren  16100  umgrpredgv  16142  isuspgren  16152  isusgren  16153  ausgrusgrben  16163  usgrf1oedg  16200  uhgr2edg  16201  usgredg3  16209  ushgredgedg  16221  ushgredgedgloop  16223  usgr0  16234  egrsubgr  16258  0grsubgr  16259  vtxdfifiun  16292  edginwlkd  16350  wlk1walkdom  16354  clwwlknon2x  16430  clwwlknonex2lem1  16432  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  ex-ceil  16494  ex-gcd  16499  bj-charfundcALT  16579  bdceqir  16614  bj-ssom  16706  trilpolemgt1  16823  redcwlpolemeq1  16839