Theorem rspcsbnea

Description: Special case related to rspsbc . (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Assertion	rspcsbnea	|- ( ( A e. B /\ A. x e. B C =/= D ) -> [_ A / x ]_ C =/= D )

Proof

Step	Hyp	Ref	Expression
1		rspsbc	|- ( A e. B -> ( A. x e. B C =/= D -> [. A / x ]. C =/= D ) )
2		df-ne	|- ( C =/= D <-> -. C = D )
3	2	sbcbii	|- ( [. A / x ]. C =/= D <-> [. A / x ]. -. C = D )
4	3	a1i	|- ( A e. B -> ( [. A / x ]. C =/= D <-> [. A / x ]. -. C = D ) )
5		sbcng	|- ( A e. B -> ( [. A / x ]. -. C = D <-> -. [. A / x ]. C = D ) )
6		sbceq1g	|- ( A e. B -> ( [. A / x ]. C = D <-> [_ A / x ]_ C = D ) )
7	6	notbid	|- ( A e. B -> ( -. [. A / x ]. C = D <-> -. [_ A / x ]_ C = D ) )
8	5 7	bitrd	|- ( A e. B -> ( [. A / x ]. -. C = D <-> -. [_ A / x ]_ C = D ) )
9	4 8	bitrd	|- ( A e. B -> ( [. A / x ]. C =/= D <-> -. [_ A / x ]_ C = D ) )
10		biidd	|- ( A e. B -> ( [_ A / x ]_ C = D <-> [_ A / x ]_ C = D ) )
11	10	necon3bbid	|- ( A e. B -> ( -. [_ A / x ]_ C = D <-> [_ A / x ]_ C =/= D ) )
12	9 11	bitrd	|- ( A e. B -> ( [. A / x ]. C =/= D <-> [_ A / x ]_ C =/= D ) )
13	1 12	sylibd	|- ( A e. B -> ( A. x e. B C =/= D -> [_ A / x ]_ C =/= D ) )
14	13	imp	|- ( ( A e. B /\ A. x e. B C =/= D ) -> [_ A / x ]_ C =/= D )