Theorem eqcomi 2242

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 2240	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

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  16062  2logb9irr  16173  2logb9irrALT  16176  sqrt2cxp2logb9e3  16177  2logb9irrap  16179  birthdaylog2  16194  cht2  16242  cht3  16243  chtublem  16261  bclbnd  16273  bposlem6  16282  bposlem8  16284  lgsdir  16325  2lgslem3a  16383  2lgslem3b  16384  2lgslem3c  16385  2lgslem3d  16386  2lgslem3d1  16390  2lgsoddprmlem3d  16400  2sqlem9  16414  2sqlem10  16415  setsvtx  16463  edgiedgbg  16477  edg0iedg0g  16478  isuhgrm  16483  isushgrm  16484  uhgr0  16497  isupgren  16507  isumgren  16517  umgrpredgv  16559  isuspgren  16569  isusgren  16570  ausgrusgrben  16580  usgrf1oedg  16617  uhgr2edg  16618  usgredg3  16626  ushgredgedg  16638  ushgredgedgloop  16640  usgr0  16651  egrsubgr  16675  0grsubgr  16676  vtxdfifiun  16709  edginwlkd  16767  wlk1walkdom  16771  clwwlknon2x  16847  clwwlknonex2lem1  16849  konigsberglem1  16900  konigsberglem2  16901  konigsberglem3  16902  konigsberglem5  16904  ex-ceil  16911  ex-gcd  16916  bj-charfundcALT  17006  bdceqir  17041  bj-ssom  17133  trilpolemgt1  17260  redcwlpolemeq1  17276