Theorem nfss 3926

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 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3260	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1854	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2883  ∀wral 3051   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2811  df-nfc 2885  df-ral 3052  df-ss 3918

This theorem is referenced by:  ssrexf  4000  nfpw  4573  ssiun2s  5004  triun  5219  iunopeqop  5469  ssopab2bw  5495  ssopab2b  5497  nffr  5597  nfrel  5729  nffun  6515  nff  6658  fvmptss  6953  ssoprab2b  7427  eqoprab2bw  7428  tfis  7797  ovmptss  8035  nffrecs  8225  oawordeulem  8481  nnawordex  8565  r1val1  9698  cardaleph  9999  nfsum1  15613  nfsum  15614  nfcprod1  15831  nfcprod  15832  iunconn  23372  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  ovoliunnul  25464  limciun  25851  ssiun2sf  32634  ssrelf  32693  funimass4f  32715  fsumiunle  32910  prodindf  32944  esumiun  34251  bnj1408  35192  totbndbnd  37990  naddwordnexlem4  43643  ss2iundf  43900  iunconnlem2  45175  iinssdf  45383  rnmptssbi  45504  stoweidlem53  46297  stoweidlem57  46301  meaiunincf  46727  meaiuninc3  46729  opnvonmbllem2  46877  smflim  47021  nfsetrecs  49931  setrec2fun  49937