Theorem nfss 4001

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893  ∀wral 3067   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895  df-ral 3068  df-ss 3993

This theorem is referenced by:  ssrexf  4075  nfpw  4641  ssiun2s  5071  triun  5298  iunopeqop  5540  ssopab2bw  5566  ssopab2b  5568  nffr  5673  nfrel  5803  nffun  6601  nff  6743  fvmptss  7041  ssoprab2b  7519  eqoprab2bw  7520  tfis  7892  ovmptss  8134  nffrecs  8324  nfwrecsOLD  8358  oawordeulem  8610  nnawordex  8693  r1val1  9855  cardaleph  10158  nfsum1  15738  nfsum  15739  nfcprod1  15956  nfcprod  15957  iunconn  23457  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  ovoliunnul  25561  limciun  25949  ssiun2sf  32582  ssrelf  32637  funimass4f  32656  fsumiunle  32833  prodindf  33987  esumiun  34058  bnj1408  35012  totbndbnd  37749  naddwordnexlem4  43363  ss2iundf  43621  iunconnlem2  44906  iinssdf  45041  rnmptssbi  45170  stoweidlem53  45974  stoweidlem57  45978  meaiunincf  46404  meaiuninc3  46406  opnvonmbllem2  46554  smflim  46698  nfsetrecs  48778  setrec2fun  48784