Theorem nfss 3915

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884  ∀wral 3052   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053  df-ss 3907

This theorem is referenced by:  ssrexf  3989  nfpw  4561  ssiun2s  4992  triun  5207  iunopeqop  5469  ssopab2bw  5495  ssopab2b  5497  nffr  5597  nfrel  5729  nffun  6515  nff  6658  fvmptss  6954  ssoprab2b  7429  eqoprab2bw  7430  tfis  7799  ovmptss  8036  nffrecs  8226  oawordeulem  8482  nnawordex  8566  r1val1  9701  cardaleph  10002  nfsum1  15643  nfsum  15644  nfcprod1  15864  nfcprod  15865  iunconn  23403  ovolfiniun  25478  ovoliunlem3  25481  ovoliun  25482  ovoliun2  25483  ovoliunnul  25484  limciun  25871  ssiun2sf  32644  ssrelf  32703  funimass4f  32725  fsumiunle  32917  prodindf  32937  esumiun  34254  bnj1408  35194  totbndbnd  38124  naddwordnexlem4  43847  ss2iundf  44104  iunconnlem2  45379  iinssdf  45587  rnmptssbi  45707  stoweidlem53  46499  stoweidlem57  46503  meaiunincf  46929  meaiuninc3  46931  opnvonmbllem2  47079  smflim  47223  nfsetrecs  50173  setrec2fun  50179