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

Proof

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