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  4153  breqtrri  4157  breqtrrdi  4172  opwo0id  4389  pwin  4427  limon  4660  tfis  4730  dfdm2  5322  cnvresid  5455  fores  5625  funcoeqres  5670  f1oprg  5685  fvmbr  5731  fnmptfvd  5813  funopdmsn  5895  fmptpr  5907  fsnunres  5917  idref  5962  riotaeqimp  6063  riotaprop  6064  fo1st  6391  fo2nd  6392  fnmpoovd  6451  ixpsnf1o  7018  phplem4  7156  snnen2og  7160  phplem4on  7169  pw1dc0el  7218  ss1o0el1o  7220  sbthlemi5  7278  eldju  7408  casefun  7425  omp1eomlem  7434  exmidfodomrlemim  7553  caucvgsrlembound  8161  ax0id  8245  1p1e2  9421  1e2m1  9423  2p1e3  9438  3p1e4  9440  4p1e5  9441  5p1e6  9442  6p1e7  9443  7p1e8  9444  8p1e9  9445  div4p1lem1div2  9559  0mnnnnn0  9595  zeo  9751  num0u  9787  numsucc  9816  decsucc  9817  1e0p1  9818  nummac  9821  decsubi  9839  decmul1  9840  decmul10add  9845  6p5lem  9846  10m1e9  9872  5t5e25  9879  6t6e36  9884  8t6e48  9895  decbin3  9918  infrenegsupex  9994  ige3m2fz  10454  fseq1p1m1  10501  fz0tp  10529  fz0to4untppr  10531  1fv  10546  fzo0to42pr  10638  fzosplitpr  10652  fzosplitprm1  10653  fldiv4lem1div2uz2  10741  xnn0nnen  10874  expnegap0  10984  sq4e2t8  11074  3dec  11152  fihashen1  11238  pr0hash2ex  11256  fundm2domnop0  11300  pfxccat3  11506  swrdccat  11507  pfxccatpfx2  11509  swrdccat3blem  11511  swrdccat3b  11512  cats2catd  11541  imi  11666  infxrnegsupex  12029  zsumdc  12151  fsumadd  12173  hashrabrex  12248  ntrivcvgap  12315  fprodmul  12358  fproddivapf  12398  fprodmodd  12408  efsep  12458  3dvds  12631  3dvdsdec  12632  3dvds2dec  12633  flodddiv4  12703  lcmneg  12852  dec2dvds  13190  2exp5  13211  2exp11  13215  ballotfilemth  13281  ennnfonelem1  13298  nninfdclemp1  13341  ndxid  13376  2strstr1g  13476  srgfcl  14277  isrhm  14465  issubrng  14507  rmodislmod  14688  cnfld0  14908  cnfld1  14909  cnfldplusf  14911  cnfldui  14924  isassa  15002  assamulgscmlem2  15042  toponrestid  15122  istpsi  15140  distopon  15188  distps  15192  discld  15237  txbas  15359  txdis  15378  txdis1cn  15379  txhmeo  15420  txswaphmeolem  15421  dvmptidcn  15815  dvmptid  15817  sinq34lt0t  15932  loge  15968  2logb9irr  16073  2logb9irrALT  16076  sqrt2cxp2logb9e3  16077  2logb9irrap  16079  birthdaylog2  16090  lgsdir  16154  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2lgsoddprmlem3d  16229  2sqlem9  16243  2sqlem10  16244  setsvtx  16292  edgiedgbg  16306  edg0iedg0g  16307  isuhgrm  16312  isushgrm  16313  uhgr0  16326  isupgren  16336  isumgren  16346  umgrpredgv  16388  isuspgren  16398  isusgren  16399  ausgrusgrben  16409  usgrf1oedg  16446  uhgr2edg  16447  usgredg3  16455  ushgredgedg  16467  ushgredgedgloop  16469  usgr0  16480  egrsubgr  16504  0grsubgr  16505  vtxdfifiun  16538  edginwlkd  16596  wlk1walkdom  16600  clwwlknon2x  16676  clwwlknonex2lem1  16678  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  ex-ceil  16740  ex-gcd  16745  bj-charfundcALT  16835  bdceqir  16870  bj-ssom  16962  trilpolemgt1  17088  redcwlpolemeq1  17104