Theorem eqcomi 2235

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  eqtr2i  2253  eqtr3i  2254  eqtr4i  2255  eqtr3id  2278  eqtr3di  2279  eqtr4di  2282  eqtr4id  2283  eqeltrri  2305  eleqtrri  2307  eqeltrrid  2319  eleqtrrdi  2325  abid2  2352  abid2f  2400  eqnetrri  2427  neeqtrri  2431  eqsstrri  3260  sseqtrri  3262  eqsstrrid  3274  sseqtrrdi  3276  difdif2ss  3464  inrab2  3480  dfopg  3860  opid  3880  eqbrtrri  4111  breqtrri  4115  breqtrrdi  4130  opwo0id  4341  pwin  4379  limon  4611  tfis  4681  dfdm2  5271  cnvresid  5404  fores  5569  funcoeqres  5614  f1oprg  5629  fvmbr  5674  fnmptfvd  5751  funopdmsn  5833  fmptpr  5845  fsnunres  5855  idref  5896  riotaeqimp  5995  riotaprop  5996  fo1st  6319  fo2nd  6320  fnmpoovd  6379  ixpsnf1o  6904  phplem4  7040  snnen2og  7044  phplem4on  7053  pw1dc0el  7102  ss1o0el1o  7104  sbthlemi5  7159  eldju  7266  casefun  7283  omp1eomlem  7292  exmidfodomrlemim  7411  caucvgsrlembound  8013  ax0id  8097  1p1e2  9259  1e2m1  9261  2p1e3  9276  3p1e4  9278  4p1e5  9279  5p1e6  9280  6p1e7  9281  7p1e8  9282  8p1e9  9283  div4p1lem1div2  9397  0mnnnnn0  9433  zeo  9584  num0u  9620  numsucc  9649  decsucc  9650  1e0p1  9651  nummac  9654  decsubi  9672  decmul1  9673  decmul10add  9678  6p5lem  9679  10m1e9  9705  5t5e25  9712  6t6e36  9717  8t6e48  9728  decbin3  9751  infrenegsupex  9827  ige3m2fz  10283  fseq1p1m1  10328  fz0tp  10356  fz0to4untppr  10358  1fv  10373  fzo0to42pr  10464  fzosplitpr  10478  fzosplitprm1  10479  fldiv4lem1div2uz2  10565  xnn0nnen  10698  expnegap0  10808  sq4e2t8  10898  3dec  10975  fihashen1  11060  pr0hash2ex  11078  fundm2domnop0  11108  pfxccat3  11314  swrdccat  11315  pfxccatpfx2  11317  swrdccat3blem  11319  swrdccat3b  11320  cats2catd  11349  imi  11460  infxrnegsupex  11823  zsumdc  11944  fsumadd  11966  hashrabrex  12041  ntrivcvgap  12108  fprodmul  12151  fproddivapf  12191  fprodmodd  12201  efsep  12251  3dvds  12424  3dvdsdec  12425  3dvds2dec  12426  flodddiv4  12496  lcmneg  12645  dec2dvds  12983  2exp5  13004  2exp11  13008  ennnfonelem1  13027  nninfdclemp1  13070  ndxid  13105  2strstr1g  13204  srgfcl  13985  isrhm  14171  issubrng  14212  rmodislmod  14364  cnfld0  14584  cnfld1  14585  cnfldplusf  14587  cnfldui  14602  toponrestid  14744  istpsi  14762  distopon  14810  distps  14814  discld  14859  txbas  14981  txdis  15000  txdis1cn  15001  txhmeo  15042  txswaphmeolem  15043  dvmptidcn  15437  dvmptid  15439  sinq34lt0t  15554  loge  15590  2logb9irr  15694  2logb9irrALT  15697  sqrt2cxp2logb9e3  15698  2logb9irrap  15700  lgsdir  15763  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3d1  15828  2lgsoddprmlem3d  15838  2sqlem9  15852  2sqlem10  15853  setsvtx  15901  edgiedgbg  15915  edg0iedg0g  15916  isuhgrm  15921  isushgrm  15922  uhgr0  15935  isupgren  15945  isumgren  15955  umgrpredgv  15997  isuspgren  16007  isusgren  16008  ausgrusgrben  16018  usgrf1oedg  16055  uhgr2edg  16056  usgredg3  16064  ushgredgedg  16076  ushgredgedgloop  16078  usgr0  16089  egrsubgr  16113  0grsubgr  16114  vtxdfifiun  16147  edginwlkd  16205  wlk1walkdom  16209  clwwlknon2x  16285  clwwlknonex2lem1  16287  ex-ceil  16322  ex-gcd  16327  bj-charfundcALT  16404  bdceqir  16439  bj-ssom  16531  trilpolemgt1  16643  redcwlpolemeq1  16658