Theorem nfss 3969

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

Syntax hints:  Ⅎwnf 1777   ∈ wcel 2098  Ⅎwnfc 2875  ∀wral 3050   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-10 2129  ax-11 2146  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-clel 2802  df-nfc 2877  df-ral 3051  df-ss 3961

This theorem is referenced by:  ssrexf  4043  nfpw  4623  ssiun2s  5052  triun  5281  iunopeqop  5523  ssopab2bw  5549  ssopab2b  5551  nffr  5652  nfrel  5781  nffun  6577  nff  6719  fvmptss  7016  ssoprab2b  7489  eqoprab2bw  7490  tfis  7860  ovmptss  8098  nffrecs  8289  nfwrecsOLD  8323  oawordeulem  8575  nnawordex  8658  r1val1  9811  cardaleph  10114  nfsum1  15672  nfsum  15673  nfcprod1  15890  nfcprod  15891  iunconn  23376  ovolfiniun  25474  ovoliunlem3  25477  ovoliun  25478  ovoliun2  25479  ovoliunnul  25480  limciun  25867  ssiun2sf  32429  ssrelf  32484  funimass4f  32503  fsumiunle  32677  prodindf  33773  esumiun  33844  bnj1408  34798  totbndbnd  37393  naddwordnexlem4  42973  ss2iundf  43231  iunconnlem2  44516  iinssdf  44645  rnmptssbi  44775  stoweidlem53  45579  stoweidlem57  45583  meaiunincf  46009  meaiuninc3  46011  opnvonmbllem2  46159  smflim  46303  nfsetrecs  48303  setrec2fun  48309