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