This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psasym

Description: A poset is antisymmetric. (Contributed by NM, 12-May-2008)

		Ref	Expression
	Assertion	psasym	$⊢ (R \in PosetRel \land A R B \land B R A) \to A = B$

Step	Hyp	Ref	Expression
1		pslem	$⊢ R \in PosetRel \to (((A R B \land B R A) \to A R A) \land (A \in ⋃ ⋃ R \to A R A) \land ((A R B \land B R A) \to A = B))$
2	1	simp3d	$⊢ R \in PosetRel \to ((A R B \land B R A) \to A = B)$
3	2	3impib	$⊢ (R \in PosetRel \land A R B \land B R A) \to A = B$