Theorem nfss 3924

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2105  Ⅎwnfc 2884  ∀wral 3061   ⊆ wss 3898

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  ssrexf  3996  nfpw  4566  ssiun2s  4995  triun  5224  iunopeqop  5465  ssopab2bw  5491  ssopab2b  5493  nffr  5594  nfrel  5721  nffun  6507  nff  6647  fvmptss  6943  ssoprab2b  7406  eqoprab2bw  7407  tfis  7769  ovmptss  8001  nffrecs  8169  nfwrecsOLD  8203  oawordeulem  8456  nnawordex  8539  r1val1  9643  cardaleph  9946  nfsum1  15500  nfsum  15501  nfsumOLD  15502  nfcprod1  15719  nfcprod  15720  iunconn  22685  ovolfiniun  24771  ovoliunlem3  24774  ovoliun  24775  ovoliun2  24776  ovoliunnul  24777  limciun  25164  ssiun2sf  31186  ssrelf  31242  funimass4f  31259  fsumiunle  31430  prodindf  32289  esumiun  32360  bnj1408  33315  totbndbnd  36060  ss2iundf  41597  iunconnlem2  42885  iinssdf  43018  rnmptssbi  43144  stoweidlem53  43939  stoweidlem57  43943  meaiunincf  44367  meaiuninc3  44369  opnvonmbllem2  44517  smflim  44661  nfsetrecs  46752  setrec2fun  46758