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 ( [ 𝐴 / 𝑥 ] 𝐵 ≠ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

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