Theorem equcom 1129

Description: Commutative law for equality.

Assertion

Ref	Expression
equcom	|- (x = y <-> y = x)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1128	. 2 |- (x = y -> y = x)
2		equcomi 1128	. 2 |- (y = x -> x = y)
3	1, 2	impbi 157	1 |- (x = y <-> y = x)

Syntax hints:   <-> wb 146   = wceq 956

This theorem is referenced by:  sbequ12r 1182  a12lem2 1377  eu1 1392  2eu6 1454  iunid 2603  dfid3 2836  relop 3275  mapsnen 4429  brdom7disj 4804  znnen 7502  ghomf1olem 10396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-8 964  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain