Theorem cleqcomi 1105

Description: Inference from commutative law for class equality.

Hypothesis

Ref	Expression
cleqcomi.1	⊢ A = B

Assertion

Ref	Expression
cleqcomi	⊢ B = A

Proof of Theorem cleqcomi

Step	Hyp	Ref	Expression
1		cleqcomi.1	. 2 ⊢ A = B
2		cleqcom 1103	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	mpbi 164	1 ⊢ B = A

Syntax hints:   = wceq 1091

This theorem is referenced by:  eqtr2 1120  eqtr3 1121  eqtr4 1122  syl5eqr 1138  syl5reqr 1139  syl6eqr 1142  syl6reqr 1143  eqeltrr 1160  eleqtrr 1162  abid2 1186  eqsstr3 1531  sseqtr4 1533  3sstr4 1539  3sstr4g 1541  syl5ssr 1545  syl6ssr 1547  birabrdv 1648  unrab 1694  elsncg 1825  pwin 1915  eqbrtrr 2078  breqtrr 2082  supub 2160  suplub 2161  tfis 2245  limon 2342  unizlim 2364  orduninsuc 2365  fores 2794  fo1st 3094  fo2nd 3095  om0r 3142  undom 3342  sbthlem5 3353  phplem5 3407  rankpw 3528  fodomb 3615  cardnum 3694  axrecex 4079  subdi 4182  lesub0 4341  subge0 4342  eqneg 4378  halfpos 4421  sqrlem11 4741  sqr4 4772  sqr9 4773  sqr2irrlem4 4780  crre 4806  crim 4807  reim0 4809  cjmul 4819  infxpidmlem7 4939  infunabs 4946  infcdaabs 4947  hvsubcan2 5036  normlem1 5063  normlem2 5064  bcseq 5073  normpar2 5100  ococ 5252  pjpj0 5259  pjococ 5272  shscl 5282  shlub 5347  fh1 5518  fh2 5519  qlax1 5520  qlaxr1 5525  osum 5538  5oa 5551  hosd1 5623  pjin1 5646  stadd 5687  hatomistic 5755

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org