Theorem eqcomi 2242

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  eqtr3id  2285  eqtr3di  2286  eqtr4di  2289  eqtr4id  2290  eqeltrri  2312  eleqtrri  2314  eqeltrrid  2326  eleqtrrdi  2332  abid2  2361  abid2f  2418  eqnetrri  2445  neeqtrri  2449  eqsstrri  3281  sseqtrri  3283  eqsstrrid  3295  sseqtrrdi  3297  difdif2ss  3488  inrab2  3506  dfopg  3902  opid  3922  eqbrtrri  4154  breqtrri  4158  breqtrrdi  4173  opwo0id  4391  pwin  4429  limon  4662  tfis  4732  dfdm2  5325  cnvresid  5458  fores  5628  funcoeqres  5673  f1oprg  5688  fvmbr  5734  fnmptfvd  5816  funopdmsn  5898  fmptpr  5910  fsnunres  5920  idref  5965  riotaeqimp  6066  riotaprop  6067  fo1st  6395  fo2nd  6396  fnmpoovd  6455  ixpsnf1o  7022  phplem4  7160  snnen2og  7164  phplem4on  7173  pw1dc0el  7222  ss1o0el1o  7224  sbthlemi5  7283  eldju  7414  casefun  7431  omp1eomlem  7440  exmidfodomrlemim  7559  caucvgsrlembound  8167  ax0id  8251  1p1e2  9430  1e2m1  9432  2p1e3  9447  3p1e4  9449  4p1e5  9450  5p1e6  9451  6p1e7  9452  7p1e8  9453  8p1e9  9454  div4p1lem1div2  9570  0mnnnnn0  9606  zeo  9762  num0u  9798  numsucc  9832  decsucc  9833  1e0p1  9834  nummac  9837  decsubi  9855  decmul1  9856  decmul10add  9861  6p5lem  9862  10m1e9  9888  5t5e25  9895  6t6e36  9900  8t6e48  9911  decbin3  9934  infrenegsupex  10010  ige3m2fz  10471  fseq1p1m1  10518  fz0tp  10546  fz0to4untppr  10548  1fv  10563  fzo0to42pr  10655  fzosplitpr  10669  fzosplitprm1  10670  fldiv4lem1div2uz2  10762  xnn0nnen  10895  expnegap0  11005  sq4e2t8  11095  3dec  11174  fihashen1  11260  pr0hash2ex  11278  fundm2domnop0  11322  pfxccat3  11528  swrdccat  11529  pfxccatpfx2  11531  swrdccat3blem  11533  swrdccat3b  11534  cats2catd  11563  imi  11688  infxrnegsupex  12054  zsumdc  12176  fsumadd  12198  hashrabrex  12273  ntrivcvgap  12340  fprodmul  12383  fproddivapf  12423  fprodmodd  12433  efsep  12483  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  flodddiv4  12728  lcmneg  12877  dec2dvds  13219  2exp5  13241  2exp11  13245  1259prm  13276  ballotfilemth  13339  ennnfonelem1  13356  nninfdclemp1  13399  ndxid  13434  2strstr1g  13535  srgfcl  14384  isrhm  14574  issubrng  14616  rmodislmod  14797  cnfld0  15017  cnfld1  15018  cnfldplusf  15020  cnfldui  15033  isassa  15111  assamulgscmlem2  15151  toponrestid  15247  istpsi  15265  distopon  15313  distps  15317  discld  15362  txbas  15484  txdis  15503  txdis1cn  15504  txhmeo  15545  txswaphmeolem  15546  dvmptidcn  15940  dvmptid  15942  sinq34lt0t  16058  loge  16096  2logb9irr  16207  2logb9irrALT  16210  sqrt2cxp2logb9e3  16211  2logb9irrap  16213  birthdaylog2  16228  cht2  16276  cht3  16277  chtublem  16295  bclbnd  16307  bposlem6  16316  bposlem8  16318  lgsdir  16359  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3d1  16424  2lgsoddprmlem3d  16434  2sqlem9  16448  2sqlem10  16449  setsvtx  16497  edgiedgbg  16511  edg0iedg0g  16512  isuhgrm  16517  isushgrm  16518  uhgr0  16531  isupgren  16541  isumgren  16551  umgrpredgv  16593  isuspgren  16603  isusgren  16604  ausgrusgrben  16614  usgrf1oedg  16651  uhgr2edg  16652  usgredg3  16660  ushgredgedg  16672  ushgredgedgloop  16674  usgr0  16685  egrsubgr  16709  0grsubgr  16710  vtxdfifiun  16743  edginwlkd  16801  wlk1walkdom  16805  clwwlknon2x  16881  clwwlknonex2lem1  16883  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  ex-ceil  16945  ex-gcd  16950  bj-charfundcALT  17040  bdceqir  17075  bj-ssom  17167  trilpolemgt1  17295  redcwlpolemeq1  17311