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

Metamath Proof Explorer

Theorem sbcne12

Description: Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion sbcne12 ⊢ [˙A / x]˙ B ≠ C ↔ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 nne ⊢ ¬ B ≠ C ↔ B = C
2 1 sbcbii ⊢ [˙A / x]˙ ¬ B ≠ C ↔ [˙A / x]˙ B = C
3 2 a1i ⊢ A ∈ V → [˙A / x]˙ ¬ B ≠ C ↔ [˙A / x]˙ B = C
4 sbcng ⊢ A ∈ V → [˙A / x]˙ ¬ B ≠ C ↔ ¬ [˙A / x]˙ B ≠ C
5 sbceqg ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C
6 nne ⊢ ¬ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C
7 5 6 bitr4di ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ¬ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C
8 3 4 7 3bitr3d ⊢ A ∈ V → ¬ [˙A / x]˙ B ≠ C ↔ ¬ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C
9 8 con4bid ⊢ A ∈ V → [˙A / x]˙ B ≠ C ↔ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C
10 sbcex ⊢ [˙A / x]˙ B ≠ C → A ∈ V
11 10 con3i ⊢ ¬ A ∈ V → ¬ [˙A / x]˙ B ≠ C
12 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ B = ∅
13 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ C = ∅
14 12 13 eqtr4d ⊢ ¬ A ∈ V → ⦋ A / x⦌ B = ⦋ A / x⦌ C
15 14 6 sylibr ⊢ ¬ A ∈ V → ¬ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C
16 11 15 2falsed ⊢ ¬ A ∈ V → [˙A / x]˙ B ≠ C ↔ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C
17 9 16 pm2.61i ⊢ [˙A / x]˙ B ≠ C ↔ ⦋ A / x⦌ B ≠ ⦋ A / x⦌ C