Theorem nfss 3924

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2908  ∀wral 3077   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910  df-ral 3078  df-ss 3916

This theorem is used by:  ssrexf  3998  nfpw  4576  ssiun2s  5007  triun  5227  iunopeqop  5494  iunopeqopOLD  5495  ssopab2bw  5522  ssopab2b  5524  nffr  5624  nfrel  5756  nffun  6560  nff  6703  fvmptss  7004  ssoprab2b  7487  eqoprab2bw  7488  tfis  7864  ovmptss  8102  nffrecs  8294  oawordeulem  8555  nnawordex  8639  r1val1  9786  setrec2fun  9966  cardaleph  10161  nfsum1  15850  nfsum  15851  nfcprod1  16070  nfcprod  16071  iunconn  23739  ovolfiniun  25815  ovoliunlem3  25818  ovoliun  25819  ovoliun2  25820  ovoliunnul  25821  limciun  26207  ssiun2sf  33147  ssrelf  33202  funimass4f  33224  fsumiunle  33413  prodindf  33422  esumiun  34719  bnj1408  35659  totbndbnd  38703  naddwordnexlem4  44387  ss2iundf  44644  iunconnlem2  45902  iinssdf  46123  rnmptssbi  46241  stoweidlem53  47032  stoweidlem57  47036  meaiunincf  47462  meaiuninc3  47464  opnvonmbllem2  47612  smflim  47756  nfsetrecs  50758