Theorem nfss 3942

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877  ∀wral 3045   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2804  df-nfc 2879  df-ral 3046  df-ss 3934

This theorem is referenced by:  ssrexf  4016  nfpw  4585  ssiun2s  5015  triun  5232  iunopeqop  5484  ssopab2bw  5510  ssopab2b  5512  nffr  5614  nfrel  5745  nffun  6542  nff  6687  fvmptss  6983  ssoprab2b  7461  eqoprab2bw  7462  tfis  7834  ovmptss  8075  nffrecs  8265  oawordeulem  8521  nnawordex  8604  r1val1  9746  cardaleph  10049  nfsum1  15663  nfsum  15664  nfcprod1  15881  nfcprod  15882  iunconn  23322  ovolfiniun  25409  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovoliunnul  25415  limciun  25802  ssiun2sf  32495  ssrelf  32550  funimass4f  32568  fsumiunle  32761  prodindf  32793  esumiun  34091  bnj1408  35033  totbndbnd  37790  naddwordnexlem4  43397  ss2iundf  43655  iunconnlem2  44931  iinssdf  45140  rnmptssbi  45261  stoweidlem53  46058  stoweidlem57  46062  meaiunincf  46488  meaiuninc3  46490  opnvonmbllem2  46638  smflim  46782  nfsetrecs  49679  setrec2fun  49685