Theorem nfss 3907

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

Hypotheses

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

Assertion

Ref	Expression
nfss	⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Proof of Theorem nfss

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfss2f.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss3f 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3183	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1854	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936  ∀wral 3106   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  ssrexf  3979  nfpw  4518  ssiun2s  4935  triun  5149  iunopeqop  5376  ssopab2bw  5399  ssopab2b  5401  nffr  5493  nfrel  5618  nffun  6347  nff  6483  fvmptss  6757  ssoprab2b  7202  eqoprab2bw  7203  tfis  7549  ovmptss  7771  nfwrecs  7932  oawordeulem  8163  nnawordex  8246  r1val1  9199  cardaleph  9500  nfsum1  15038  nfsum  15039  nfsumOLD  15040  nfcprod1  15256  nfcprod  15257  iunconn  22033  ovolfiniun  24105  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  ovoliunnul  24111  limciun  24497  ssiun2sf  30323  ssrelf  30379  funimass4f  30396  fsumiunle  30571  prodindf  31392  esumiun  31463  bnj1408  32418  nffrecs  33233  totbndbnd  35227  ss2iundf  40360  iunconnlem2  41641  iinssdf  41776  rnmptssbi  41899  stoweidlem53  42695  stoweidlem57  42699  meaiunincf  43122  meaiuninc3  43124  opnvonmbllem2  43272  smflim  43410  nfsetrecs  45216  setrec2fun  45222