New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqcomi GIF version

Theorem eqcomi 2357
 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
StepHypRef Expression
1 eqcomi.1 . 2 A = B
2 eqcom 2355 . 2 (A = BB = A)
31, 2mpbi 199 1 B = A
 Colors of variables: wff setvar class Syntax hints:   = wceq 1642 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-cleq 2346 This theorem is referenced by:  eqtr2i  2374  eqtr3i  2375  eqtr4i  2376  syl5eqr  2399  syl5reqr  2400  syl6eqr  2403  syl6reqr  2404  eqeltrri  2424  eleqtrri  2426  syl5eqelr  2438  syl6eleqr  2444  abid2  2470  abid2f  2514  eqnetrri  2535  neeqtrri  2539  eqsstr3i  3302  sseqtr4i  3304  syl5eqssr  3316  syl6sseqr  3318  inrab2  3528  pw1eqadj  4332  nnsucelrlem3  4426  nulge  4456  ltfinirr  4457  ltfinp1  4462  lefinlteq  4463  lefinrflx  4467  ncfinprop  4474  0ceven  4505  eqbrtrri  4660  breqtrri  4664  syl6breqr  4679  cnvresid  5166  fores  5278  1st2nd2  5516  fnfullfun  5858  clos1basesuc  5882  ncaddccl  6144  ce0t  6232  nchoicelem9  6297  nchoicelem19  6307
 Copyright terms: Public domain W3C validator