Theorem nfss 3931

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2146  Ⅎwnfc 2912  ∀wral 3081   ⊆ wss 3906

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 2148  ax-10 2179  ax-11 2195  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2840  df-nfc 2914  df-ral 3082  df-ss 3923

This theorem is used by:  ssrexf  4005  nfpw  4583  ssiun2s  5015  triun  5235  iunopeqop  5506  iunopeqopOLD  5507  ssopab2bw  5534  ssopab2b  5536  nffr  5636  nfrel  5768  nffun  6563  nff  6705  fvmptss  7006  ssoprab2b  7485  eqoprab2bw  7486  tfis  7853  ovmptss  8090  nffrecs  8282  oawordeulem  8541  nnawordex  8625  r1val1  9761  cardaleph  10085  nfsum1  15760  nfsum  15761  nfcprod1  15980  nfcprod  15981  iunconn  23614  ovolfiniun  25689  ovoliunlem3  25692  ovoliun  25693  ovoliun2  25694  ovoliunnul  25695  limciun  26082  ssiun2sf  32933  ssrelf  32989  funimass4f  33011  fsumiunle  33202  prodindf  33211  esumiun  34507  bnj1408  35448  totbndbnd  38473  naddwordnexlem4  44161  ss2iundf  44418  iunconnlem2  45676  iinssdf  45890  rnmptssbi  46008  stoweidlem53  46800  stoweidlem57  46804  meaiunincf  47230  meaiuninc3  47232  opnvonmbllem2  47380  smflim  47524  nfsetrecs  50497  setrec2fun  50503