Theorem nfss 3927

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879  ∀wral 3047   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048  df-ss 3919

This theorem is referenced by:  ssrexf  4001  nfpw  4569  ssiun2s  4997  triun  5212  iunopeqop  5461  ssopab2bw  5487  ssopab2b  5489  nffr  5589  nfrel  5720  nffun  6504  nff  6647  fvmptss  6941  ssoprab2b  7415  eqoprab2bw  7416  tfis  7785  ovmptss  8023  nffrecs  8213  oawordeulem  8469  nnawordex  8552  r1val1  9679  cardaleph  9980  nfsum1  15597  nfsum  15598  nfcprod1  15815  nfcprod  15816  iunconn  23344  ovolfiniun  25430  ovoliunlem3  25433  ovoliun  25434  ovoliun2  25435  ovoliunnul  25436  limciun  25823  ssiun2sf  32537  ssrelf  32596  funimass4f  32617  fsumiunle  32810  prodindf  32842  esumiun  34105  bnj1408  35046  totbndbnd  37835  naddwordnexlem4  43440  ss2iundf  43698  iunconnlem2  44973  iinssdf  45182  rnmptssbi  45303  stoweidlem53  46097  stoweidlem57  46101  meaiunincf  46527  meaiuninc3  46529  opnvonmbllem2  46677  smflim  46821  nfsetrecs  49724  setrec2fun  49730