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  9423  1e2m1  9425  2p1e3  9440  3p1e4  9442  4p1e5  9443  5p1e6  9444  6p1e7  9445  7p1e8  9446  8p1e9  9447  div4p1lem1div2  9563  0mnnnnn0  9599  zeo  9755  num0u  9791  numsucc  9825  decsucc  9826  1e0p1  9827  nummac  9830  decsubi  9848  decmul1  9849  decmul10add  9854  6p5lem  9855  10m1e9  9881  5t5e25  9888  6t6e36  9893  8t6e48  9904  decbin3  9927  infrenegsupex  10003  ige3m2fz  10464  fseq1p1m1  10511  fz0tp  10539  fz0to4untppr  10541  1fv  10556  fzo0to42pr  10648  fzosplitpr  10662  fzosplitprm1  10663  fldiv4lem1div2uz2  10754  xnn0nnen  10887  expnegap0  10997  sq4e2t8  11087  3dec  11166  fihashen1  11252  pr0hash2ex  11270  fundm2domnop0  11314  pfxccat3  11520  swrdccat  11521  pfxccatpfx2  11523  swrdccat3blem  11525  swrdccat3b  11526  cats2catd  11555  imi  11680  infxrnegsupex  12045  zsumdc  12167  fsumadd  12189  hashrabrex  12264  ntrivcvgap  12331  fprodmul  12374  fproddivapf  12414  fprodmodd  12424  efsep  12474  3dvds  12647  3dvdsdec  12648  3dvds2dec  12649  flodddiv4  12719  lcmneg  12868  dec2dvds  13210  2exp5  13232  2exp11  13236  1259prm  13267  ballotfilemth  13330  ennnfonelem1  13347  nninfdclemp1  13390  ndxid  13425  2strstr1g  13525  srgfcl  14326  isrhm  14514  issubrng  14556  rmodislmod  14737  cnfld0  14957  cnfld1  14958  cnfldplusf  14960  cnfldui  14973  isassa  15051  assamulgscmlem2  15091  toponrestid  15171  istpsi  15189  distopon  15237  distps  15241  discld  15286  txbas  15408  txdis  15427  txdis1cn  15428  txhmeo  15469  txswaphmeolem  15470  dvmptidcn  15864  dvmptid  15866  sinq34lt0t  15982  loge  16018  2logb9irr  16126  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  birthdaylog2  16147  bclbnd  16205  lgsdir  16252  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3d1  16317  2lgsoddprmlem3d  16327  2sqlem9  16341  2sqlem10  16342  setsvtx  16390  edgiedgbg  16404  edg0iedg0g  16405  isuhgrm  16410  isushgrm  16411  uhgr0  16424  isupgren  16434  isumgren  16444  umgrpredgv  16486  isuspgren  16496  isusgren  16497  ausgrusgrben  16507  usgrf1oedg  16544  uhgr2edg  16545  usgredg3  16553  ushgredgedg  16565  ushgredgedgloop  16567  usgr0  16578  egrsubgr  16602  0grsubgr  16603  vtxdfifiun  16636  edginwlkd  16694  wlk1walkdom  16698  clwwlknon2x  16774  clwwlknonex2lem1  16776  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  ex-ceil  16838  ex-gcd  16843  bj-charfundcALT  16933  bdceqir  16968  bj-ssom  17060  trilpolemgt1  17186  redcwlpolemeq1  17202