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	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		snnen2o	⊢ ¬ { 𝐴 } ≈ 2o
2		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
3		preq2	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
4	2 3	eqtr2id	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
5	4	breq1d	⊢ ( 𝐴 = 𝐵 → ( { 𝐴 , 𝐵 } ≈ 2o ↔ { 𝐴 } ≈ 2o ) )
6	1 5	mtbiri	⊢ ( 𝐴 = 𝐵 → ¬ { 𝐴 , 𝐵 } ≈ 2o )
7	6	necon2ai	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → 𝐴 ≠ 𝐵 )
8		enpr2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
9	8	3expia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } ≈ 2o ) )
10	7 9	impbid2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )