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 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 )