Theorem eqcomi 2238

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 2236	. 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 2216

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

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  eqtr3id  2281  eqtr3di  2282  eqtr4di  2285  eqtr4id  2286  eqeltrri  2308  eleqtrri  2310  eqeltrrid  2322  eleqtrrdi  2328  abid2  2357  abid2f  2412  eqnetrri  2439  neeqtrri  2443  eqsstrri  3275  sseqtrri  3277  eqsstrrid  3289  sseqtrrdi  3291  difdif2ss  3482  inrab2  3498  dfopg  3886  opid  3906  eqbrtrri  4137  breqtrri  4141  breqtrrdi  4156  opwo0id  4370  pwin  4408  limon  4640  tfis  4710  dfdm2  5302  cnvresid  5435  fores  5605  funcoeqres  5650  f1oprg  5665  fvmbr  5710  fnmptfvd  5787  funopdmsn  5869  fmptpr  5881  fsnunres  5891  idref  5935  riotaeqimp  6036  riotaprop  6037  fo1st  6364  fo2nd  6365  fnmpoovd  6424  ixpsnf1o  6984  phplem4  7122  snnen2og  7126  phplem4on  7135  pw1dc0el  7184  ss1o0el1o  7186  sbthlemi5  7244  eldju  7372  casefun  7389  omp1eomlem  7398  exmidfodomrlemim  7517  caucvgsrlembound  8125  ax0id  8209  1p1e2  9371  1e2m1  9373  2p1e3  9388  3p1e4  9390  4p1e5  9391  5p1e6  9392  6p1e7  9393  7p1e8  9394  8p1e9  9395  div4p1lem1div2  9509  0mnnnnn0  9545  zeo  9701  num0u  9737  numsucc  9766  decsucc  9767  1e0p1  9768  nummac  9771  decsubi  9789  decmul1  9790  decmul10add  9795  6p5lem  9796  10m1e9  9822  5t5e25  9829  6t6e36  9834  8t6e48  9845  decbin3  9868  infrenegsupex  9944  ige3m2fz  10403  fseq1p1m1  10450  fz0tp  10478  fz0to4untppr  10480  1fv  10495  fzo0to42pr  10587  fzosplitpr  10601  fzosplitprm1  10602  fldiv4lem1div2uz2  10690  xnn0nnen  10823  expnegap0  10933  sq4e2t8  11023  3dec  11101  fihashen1  11187  pr0hash2ex  11205  fundm2domnop0  11245  pfxccat3  11451  swrdccat  11452  pfxccatpfx2  11454  swrdccat3blem  11456  swrdccat3b  11457  cats2catd  11486  imi  11610  infxrnegsupex  11973  zsumdc  12095  fsumadd  12117  hashrabrex  12192  ntrivcvgap  12259  fprodmul  12302  fproddivapf  12342  fprodmodd  12352  efsep  12402  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  flodddiv4  12647  lcmneg  12796  dec2dvds  13134  2exp5  13155  2exp11  13159  ballotfilemth  13225  ennnfonelem1  13242  nninfdclemp1  13285  ndxid  13320  2strstr1g  13419  srgfcl  14216  isrhm  14403  issubrng  14445  rmodislmod  14625  cnfld0  14845  cnfld1  14846  cnfldplusf  14848  cnfldui  14863  toponrestid  15012  istpsi  15030  distopon  15078  distps  15082  discld  15127  txbas  15249  txdis  15268  txdis1cn  15269  txhmeo  15310  txswaphmeolem  15311  dvmptidcn  15705  dvmptid  15707  sinq34lt0t  15822  loge  15858  2logb9irr  15962  2logb9irrALT  15965  sqrt2cxp2logb9e3  15966  2logb9irrap  15968  lgsdir  16034  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3d1  16099  2lgsoddprmlem3d  16109  2sqlem9  16123  2sqlem10  16124  setsvtx  16172  edgiedgbg  16186  edg0iedg0g  16187  isuhgrm  16192  isushgrm  16193  uhgr0  16206  isupgren  16216  isumgren  16226  umgrpredgv  16268  isuspgren  16278  isusgren  16279  ausgrusgrben  16289  usgrf1oedg  16326  uhgr2edg  16327  usgredg3  16335  ushgredgedg  16347  ushgredgedgloop  16349  usgr0  16360  egrsubgr  16384  0grsubgr  16385  vtxdfifiun  16418  edginwlkd  16476  wlk1walkdom  16480  clwwlknon2x  16556  clwwlknonex2lem1  16558  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  ex-ceil  16620  ex-gcd  16625  bj-charfundcALT  16705  bdceqir  16740  bj-ssom  16832  trilpolemgt1  16949  redcwlpolemeq1  16965