Theorem nfss 3976

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890  ∀wral 3061   ⊆ wss 3951

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 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-ss 3968

This theorem is referenced by:  ssrexf  4050  nfpw  4619  ssiun2s  5048  triun  5274  iunopeqop  5526  ssopab2bw  5552  ssopab2b  5554  nffr  5658  nfrel  5789  nffun  6589  nff  6732  fvmptss  7028  ssoprab2b  7502  eqoprab2bw  7503  tfis  7876  ovmptss  8118  nffrecs  8308  nfwrecsOLD  8342  oawordeulem  8592  nnawordex  8675  r1val1  9826  cardaleph  10129  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  iunconn  23436  ovolfiniun  25536  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  ovoliunnul  25542  limciun  25929  ssiun2sf  32572  ssrelf  32627  funimass4f  32647  fsumiunle  32831  prodindf  32848  esumiun  34095  bnj1408  35050  totbndbnd  37796  naddwordnexlem4  43414  ss2iundf  43672  iunconnlem2  44955  iinssdf  45144  rnmptssbi  45267  stoweidlem53  46068  stoweidlem57  46072  meaiunincf  46498  meaiuninc3  46500  opnvonmbllem2  46648  smflim  46792  nfsetrecs  49205  setrec2fun  49211