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

Metamath Proof Explorer

Theorem oppcmndclem

Description: Lemma for oppcmndc . Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc are in -. x = y form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypothesis oppcmndclem.1 ⊢ φ → B = A
Assertion oppcmndclem ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ≠ Y → ψ

Proof

Step Hyp Ref Expression
1 oppcmndclem.1 ⊢ φ → B = A
2 df-ne ⊢ X ≠ Y ↔ ¬ X = Y
3 eqeq1 ⊢ x = X → x = y ↔ X = y
4 eqeq2 ⊢ y = Y → X = y ↔ X = Y
5 mosn ⊢ B = A → ∃* x x ∈ B
6 1 5 syl ⊢ φ → ∃* x x ∈ B
7 moel ⊢ ∃* x x ∈ B ↔ ∀ x ∈ B ∀ y ∈ B x = y
8 6 7 sylib ⊢ φ → ∀ x ∈ B ∀ y ∈ B x = y
9 8 adantr ⊢ φ ∧ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B x = y
10 simprl ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ∈ B
11 simprr ⊢ φ ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
12 3 4 9 10 11 rspc2dv ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X = Y
13 12 pm2.24d ⊢ φ ∧ X ∈ B ∧ Y ∈ B → ¬ X = Y → ψ
14 2 13 biimtrid ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ≠ Y → ψ