Theorem nfss

Description: If x is not free in A and B , it is not free in A C_ B . (Contributed by NM, 27-Dec-1996)

	Ref	Expression
Hypotheses	dfss2f.1	|- F/_ x A
	dfss2f.2	|- F/_ x B
Assertion	nfss	|- F/ x A C_ B

Proof

Step	Hyp	Ref	Expression
1		dfss2f.1	|- F/_ x A
2		dfss2f.2	|- F/_ x B
3	1 2	dfss3f	|- ( A C_ B <-> A. x e. A x e. B )
4		nfra1	|- F/ x A. x e. A x e. B
5	3 4	nfxfr	|- F/ x A C_ B