Metamath Proof Explorer

Theorem psasym

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

Ref Expression
Assertion psasym ⊢ R ∈ PosetRel ∧ A R B ∧ B R A → A = B

Proof

Step Hyp Ref Expression
1 pslem ⊢ R ∈ PosetRel → A R B ∧ B R A → A R A ∧ A ∈ ⋃ ⋃ R → A R A ∧ A R B ∧ B R A → A = B
2 1 simp3d ⊢ R ∈ PosetRel → A R B ∧ B R A → A = B
3 2 3impib ⊢ R ∈ PosetRel ∧ A R B ∧ B R A → A = B