Theorem nfss 3561

Description: If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)

Hypotheses

Ref	Expression
dfss2f.1	⊢ Ⅎ𝑥𝐴
dfss2f.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfss	⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Proof of Theorem nfss

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfss2f.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss3f 3560	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 2925	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1771	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738  ∀wral 2896   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-in 3547  df-ss 3554

This theorem is referenced by:  ssrexf  3628  nfpw  4120  ssiun2s  4500  triun  4694  iunopeqop  4906  ssopab2b  4927  nffr  5012  nfrel  5127  nffun  5826  nff  5954  fvmptss  6201  ssoprab2b  6610  tfis  6946  ovmptss  7145  nfwrecs  7296  oawordeulem  7521  nnawordex  7604  r1val1  8532  cardaleph  8795  nfsum1  14268  nfsum  14269  nfcprod1  14479  nfcprod  14480  iuncon  21041  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  limciun  23464  ssiun2sf  28760  ssrelf  28805  funimass4f  28818  esumiun  29483  bnj1408  30358  totbndbnd  32758  ss2iundf  36970  iunconlem2  38193  stoweidlem53  38946  stoweidlem57  38950  opnvonmbllem2  39523  smflim  39663  nfsetrecs  42232  setrec2fun  42238