Theorem eqcom 811

Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69.

Assertion

Ref	Expression
eqcom	⊢ (x = y → y = x)

Proof of Theorem eqcom

Step	Hyp	Ref	Expression
1		eqid 810	. 2 ⊢ x = x
2		ax-8 798	. 2 ⊢ (x = y → (x = x → y = x))
3	1, 2	mpi 44	1 ⊢ (x = y → y = x)

Syntax hints:   → wi 2   = weq 797

This theorem is referenced by:  eqcomb 812  eqcoms 813  eqan 816  eq4 821  cbv2 846  eqvin.l1 851  sbeq2 901  a16g 933  zfaus 1480  rext 1862  ider 3208  unxpdomlem 3649  axextnd 3737

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-6 675  ax-gen 677  ax-8 798  ax-9 799  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org