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  7409  casefun  7426  omp1eomlem  7435  exmidfodomrlemim  7554  caucvgsrlembound  8162  ax0id  8246  1p1e2  9424  1e2m1  9426  2p1e3  9441  3p1e4  9443  4p1e5  9444  5p1e6  9445  6p1e7  9446  7p1e8  9447  8p1e9  9448  div4p1lem1div2  9564  0mnnnnn0  9600  zeo  9756  num0u  9792  numsucc  9826  decsucc  9827  1e0p1  9828  nummac  9831  decsubi  9849  decmul1  9850  decmul10add  9855  6p5lem  9856  10m1e9  9882  5t5e25  9889  6t6e36  9894  8t6e48  9905  decbin3  9928  infrenegsupex  10004  ige3m2fz  10465  fseq1p1m1  10512  fz0tp  10540  fz0to4untppr  10542  1fv  10557  fzo0to42pr  10649  fzosplitpr  10663  fzosplitprm1  10664  fldiv4lem1div2uz2  10756  xnn0nnen  10889  expnegap0  10999  sq4e2t8  11089  3dec  11168  fihashen1  11254  pr0hash2ex  11272  fundm2domnop0  11316  pfxccat3  11522  swrdccat  11523  pfxccatpfx2  11525  swrdccat3blem  11527  swrdccat3b  11528  cats2catd  11557  imi  11682  infxrnegsupex  12048  zsumdc  12170  fsumadd  12192  hashrabrex  12267  ntrivcvgap  12334  fprodmul  12377  fproddivapf  12417  fprodmodd  12427  efsep  12477  3dvds  12650  3dvdsdec  12651  3dvds2dec  12652  flodddiv4  12722  lcmneg  12871  dec2dvds  13213  2exp5  13235  2exp11  13239  1259prm  13270  ballotfilemth  13333  ennnfonelem1  13350  nninfdclemp1  13393  ndxid  13428  2strstr1g  13529  srgfcl  14361  isrhm  14549  issubrng  14591  rmodislmod  14772  cnfld0  14992  cnfld1  14993  cnfldplusf  14995  cnfldui  15008  isassa  15086  assamulgscmlem2  15126  toponrestid  15213  istpsi  15231  distopon  15279  distps  15283  discld  15328  txbas  15450  txdis  15469  txdis1cn  15470  txhmeo  15511  txswaphmeolem  15512  dvmptidcn  15906  dvmptid  15908  sinq34lt0t  16024  loge  16060  2logb9irr  16168  2logb9irrALT  16171  sqrt2cxp2logb9e3  16172  2logb9irrap  16174  birthdaylog2  16189  cht2  16237  cht3  16238  chtublem  16256  bclbnd  16268  bposlem6  16277  bposlem8  16279  lgsdir  16320  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3d1  16385  2lgsoddprmlem3d  16395  2sqlem9  16409  2sqlem10  16410  setsvtx  16458  edgiedgbg  16472  edg0iedg0g  16473  isuhgrm  16478  isushgrm  16479  uhgr0  16492  isupgren  16502  isumgren  16512  umgrpredgv  16554  isuspgren  16564  isusgren  16565  ausgrusgrben  16575  usgrf1oedg  16612  uhgr2edg  16613  usgredg3  16621  ushgredgedg  16633  ushgredgedgloop  16635  usgr0  16646  egrsubgr  16670  0grsubgr  16671  vtxdfifiun  16704  edginwlkd  16762  wlk1walkdom  16766  clwwlknon2x  16842  clwwlknonex2lem1  16844  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  ex-ceil  16906  ex-gcd  16911  bj-charfundcALT  17001  bdceqir  17036  bj-ssom  17128  trilpolemgt1  17255  redcwlpolemeq1  17271