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 e. _V -> ( [. A / x ]. -. B =/= C <-> [. A / x ]. B = C ) )
4		sbcng	|- ( A e. _V -> ( [. A / x ]. -. B =/= C <-> -. [. A / x ]. B =/= C ) )
5		sbceqg	|- ( A e. _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 e. _V -> ( [. A / x ]. B = C <-> -. [_ A / x ]_ B =/= [_ A / x ]_ C ) )
8	3 4 7	3bitr3d	|- ( A e. _V -> ( -. [. A / x ]. B =/= C <-> -. [_ A / x ]_ B =/= [_ A / x ]_ C ) )
9	8	con4bid	|- ( A e. _V -> ( [. A / x ]. B =/= C <-> [_ A / x ]_ B =/= [_ A / x ]_ C ) )
10		sbcex	|- ( [. A / x ]. B =/= C -> A e. _V )
11	10	con3i	|- ( -. A e. _V -> -. [. A / x ]. B =/= C )
12		csbprc	|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
13		csbprc	|- ( -. A e. _V -> [_ A / x ]_ C = (/) )
14	12 13	eqtr4d	|- ( -. A e. _V -> [_ A / x ]_ B = [_ A / x ]_ C )
15	14 6	sylibr	|- ( -. A e. _V -> -. [_ A / x ]_ B =/= [_ A / x ]_ C )
16	11 15	2falsed	|- ( -. A e. _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 )