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

Metamath Proof Explorer

Theorem pr2ne

Description: If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 30-Dec-2024)

Ref Expression
Assertion pr2ne ⊢ A ∈ C ∧ B ∈ D → A B ≈ 2 𝑜 ↔ A ≠ B

Proof

Step Hyp Ref Expression
1 snnen2o ⊢ ¬ A ≈ 2 𝑜
2 dfsn2 ⊢ A = A A
3 preq2 ⊢ A = B → A A = A B
4 2 3 eqtr2id ⊢ A = B → A B = A
5 4 breq1d ⊢ A = B → A B ≈ 2 𝑜 ↔ A ≈ 2 𝑜
6 1 5 mtbiri ⊢ A = B → ¬ A B ≈ 2 𝑜
7 6 necon2ai ⊢ A B ≈ 2 𝑜 → A ≠ B
8 enpr2 ⊢ A ∈ C ∧ B ∈ D ∧ A ≠ B → A B ≈ 2 𝑜
9 8 3expia ⊢ A ∈ C ∧ B ∈ D → A ≠ B → A B ≈ 2 𝑜
10 7 9 impbid2 ⊢ A ∈ C ∧ B ∈ D → A B ≈ 2 𝑜 ↔ A ≠ B