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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced 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  3897  opid  3917  eqbrtrri  4148  breqtrri  4152  breqtrrdi  4167  opwo0id  4384  pwin  4422  limon  4655  tfis  4725  dfdm2  5317  cnvresid  5450  fores  5620  funcoeqres  5665  f1oprg  5680  fvmbr  5725  fnmptfvd  5804  funopdmsn  5886  fmptpr  5898  fsnunres  5908  idref  5952  riotaeqimp  6053  riotaprop  6054  fo1st  6381  fo2nd  6382  fnmpoovd  6441  ixpsnf1o  7008  phplem4  7146  snnen2og  7150  phplem4on  7159  pw1dc0el  7208  ss1o0el1o  7210  sbthlemi5  7268  eldju  7398  casefun  7415  omp1eomlem  7424  exmidfodomrlemim  7543  caucvgsrlembound  8151  ax0id  8235  1p1e2  9400  1e2m1  9402  2p1e3  9417  3p1e4  9419  4p1e5  9420  5p1e6  9421  6p1e7  9422  7p1e8  9423  8p1e9  9424  div4p1lem1div2  9538  0mnnnnn0  9574  zeo  9730  num0u  9766  numsucc  9795  decsucc  9796  1e0p1  9797  nummac  9800  decsubi  9818  decmul1  9819  decmul10add  9824  6p5lem  9825  10m1e9  9851  5t5e25  9858  6t6e36  9863  8t6e48  9874  decbin3  9897  infrenegsupex  9973  ige3m2fz  10432  fseq1p1m1  10479  fz0tp  10507  fz0to4untppr  10509  1fv  10524  fzo0to42pr  10616  fzosplitpr  10630  fzosplitprm1  10631  fldiv4lem1div2uz2  10719  xnn0nnen  10852  expnegap0  10962  sq4e2t8  11052  3dec  11130  fihashen1  11216  pr0hash2ex  11234  fundm2domnop0  11278  pfxccat3  11484  swrdccat  11485  pfxccatpfx2  11487  swrdccat3blem  11489  swrdccat3b  11490  cats2catd  11519  imi  11644  infxrnegsupex  12007  zsumdc  12129  fsumadd  12151  hashrabrex  12226  ntrivcvgap  12293  fprodmul  12336  fproddivapf  12376  fprodmodd  12386  efsep  12436  3dvds  12609  3dvdsdec  12610  3dvds2dec  12611  flodddiv4  12681  lcmneg  12830  dec2dvds  13168  2exp5  13189  2exp11  13193  ballotfilemth  13259  ennnfonelem1  13276  nninfdclemp1  13319  ndxid  13354  2strstr1g  13453  srgfcl  14251  isrhm  14438  issubrng  14480  rmodislmod  14660  cnfld0  14880  cnfld1  14881  cnfldplusf  14883  cnfldui  14896  toponrestid  15045  istpsi  15063  distopon  15111  distps  15115  discld  15160  txbas  15282  txdis  15301  txdis1cn  15302  txhmeo  15343  txswaphmeolem  15344  dvmptidcn  15738  dvmptid  15740  sinq34lt0t  15855  loge  15891  2logb9irr  15996  2logb9irrALT  15999  sqrt2cxp2logb9e3  16000  2logb9irrap  16002  lgsdir  16068  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3d1  16133  2lgsoddprmlem3d  16143  2sqlem9  16157  2sqlem10  16158  setsvtx  16206  edgiedgbg  16220  edg0iedg0g  16221  isuhgrm  16226  isushgrm  16227  uhgr0  16240  isupgren  16250  isumgren  16260  umgrpredgv  16302  isuspgren  16312  isusgren  16313  ausgrusgrben  16323  usgrf1oedg  16360  uhgr2edg  16361  usgredg3  16369  ushgredgedg  16381  ushgredgedgloop  16383  usgr0  16394  egrsubgr  16418  0grsubgr  16419  vtxdfifiun  16452  edginwlkd  16510  wlk1walkdom  16514  clwwlknon2x  16590  clwwlknonex2lem1  16592  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  ex-ceil  16654  ex-gcd  16659  bj-charfundcALT  16749  bdceqir  16784  bj-ssom  16876  trilpolemgt1  16993  redcwlpolemeq1  17009