Metamath Proof Explorer


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 𝑥 𝐴
dfss2f.2 𝑥 𝐵
Assertion nfss 𝑥 𝐴𝐵

Proof

Step Hyp Ref Expression
1 dfss2f.1 𝑥 𝐴
2 dfss2f.2 𝑥 𝐵
3 1 2 dfss3f ( 𝐴𝐵 ↔ ∀ 𝑥𝐴 𝑥𝐵 )
4 nfra1 𝑥𝑥𝐴 𝑥𝐵
5 3 4 nfxfr 𝑥 𝐴𝐵