Theorem eqcomi 2210

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2208	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  eqtr2i  2228  eqtr3i  2229  eqtr4i  2230  eqtr3id  2253  eqtr3di  2254  eqtr4di  2257  eqtr4id  2258  eqeltrri  2280  eleqtrri  2282  eqeltrrid  2294  eleqtrrdi  2300  abid2  2327  abid2f  2375  eqnetrri  2402  neeqtrri  2406  eqsstrri  3228  sseqtrri  3230  eqsstrrid  3242  sseqtrrdi  3244  difdif2ss  3432  inrab2  3448  dfopg  3820  opid  3840  eqbrtrri  4071  breqtrri  4075  breqtrrdi  4090  opwo0id  4298  pwin  4334  limon  4566  tfis  4636  dfdm2  5223  cnvresid  5354  fores  5517  funcoeqres  5562  f1oprg  5576  fnmptfvd  5694  funopdmsn  5774  fmptpr  5786  fsnunres  5796  idref  5835  riotaprop  5933  fo1st  6253  fo2nd  6254  fnmpoovd  6311  ixpsnf1o  6833  phplem4  6964  snnen2og  6968  phplem4on  6976  pw1dc0el  7020  ss1o0el1o  7022  sbthlemi5  7075  eldju  7182  casefun  7199  omp1eomlem  7208  exmidfodomrlemim  7322  caucvgsrlembound  7920  ax0id  8004  1p1e2  9166  1e2m1  9168  2p1e3  9183  3p1e4  9185  4p1e5  9186  5p1e6  9187  6p1e7  9188  7p1e8  9189  8p1e9  9190  div4p1lem1div2  9304  0mnnnnn0  9340  zeo  9491  num0u  9527  numsucc  9556  decsucc  9557  1e0p1  9558  nummac  9561  decsubi  9579  decmul1  9580  decmul10add  9585  6p5lem  9586  10m1e9  9612  5t5e25  9619  6t6e36  9624  8t6e48  9635  decbin3  9658  infrenegsupex  9728  ige3m2fz  10184  fseq1p1m1  10229  fz0tp  10257  fz0to4untppr  10259  1fv  10274  fzo0to42pr  10362  fzosplitprm1  10376  fldiv4lem1div2uz2  10462  xnn0nnen  10595  expnegap0  10705  sq4e2t8  10795  3dec  10872  fihashen1  10957  pr0hash2ex  10973  fundm2domnop0  11003  imi  11261  infxrnegsupex  11624  zsumdc  11745  fsumadd  11767  hashrabrex  11842  ntrivcvgap  11909  fprodmul  11952  fproddivapf  11992  fprodmodd  12002  efsep  12052  3dvds  12225  3dvdsdec  12226  3dvds2dec  12227  flodddiv4  12297  lcmneg  12446  dec2dvds  12784  2exp5  12805  2exp11  12809  ennnfonelem1  12828  nninfdclemp1  12871  ndxid  12906  2strstr1g  13004  srgfcl  13785  isrhm  13970  issubrng  14011  rmodislmod  14163  cnfld0  14383  cnfld1  14384  cnfldplusf  14386  cnfldui  14401  toponrestid  14543  istpsi  14561  distopon  14609  distps  14613  discld  14658  txbas  14780  txdis  14799  txdis1cn  14800  txhmeo  14841  txswaphmeolem  14842  dvmptidcn  15236  dvmptid  15238  sinq34lt0t  15353  loge  15389  2logb9irr  15493  2logb9irrALT  15496  sqrt2cxp2logb9e3  15497  2logb9irrap  15499  lgsdir  15562  2lgslem3a  15620  2lgslem3b  15621  2lgslem3c  15622  2lgslem3d  15623  2lgslem3d1  15627  2lgsoddprmlem3d  15637  2sqlem9  15651  2sqlem10  15652  edgiedgbg  15711  edg0iedg0g  15712  isuhgrm  15717  isushgrm  15718  uhgr0  15731  isupgren  15741  isumgren  15751  ex-ceil  15776  ex-gcd  15781  bj-charfundcALT  15859  bdceqir  15894  bj-ssom  15986  trilpolemgt1  16093  redcwlpolemeq1  16108