Theorem nfss 3931

Description: If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)

Hypotheses

Ref	Expression
dfssf.1	⊢ Ⅎ𝑥𝐴
dfssf.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfss	⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Proof of Theorem nfss

Step	Hyp	Ref	Expression
1		dfssf.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfssf.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss3f 3930	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3289	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1883	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910  ∀wral 3079   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080  df-ss 3923

This theorem is referenced by:  ssrexf  4005  nfpw  4582  ssiun2s  5014  triun  5234  iunopeqop  5506  iunopeqopOLD  5507  ssopab2bw  5534  ssopab2b  5536  nffr  5636  nfrel  5768  nffun  6561  nff  6703  fvmptss  7004  ssoprab2b  7481  eqoprab2bw  7482  tfis  7852  ovmptss  8089  nffrecs  8281  oawordeulem  8540  nnawordex  8624  r1val1  9759  cardaleph  10074  nfsum1  15743  nfsum  15744  nfcprod1  15964  nfcprod  15965  iunconn  23566  ovolfiniun  25641  ovoliunlem3  25644  ovoliun  25645  ovoliun2  25646  ovoliunnul  25647  limciun  26034  ssiun2sf  32885  ssrelf  32941  funimass4f  32963  fsumiunle  33154  prodindf  33163  esumiun  34465  bnj1408  35405  totbndbnd  38421  naddwordnexlem4  44111  ss2iundf  44368  iunconnlem2  45626  iinssdf  45840  rnmptssbi  45958  stoweidlem53  46750  stoweidlem57  46754  meaiunincf  47180  meaiuninc3  47182  opnvonmbllem2  47330  smflim  47474  nfsetrecs  50447  setrec2fun  50453