Theorem nfss 3928

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

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

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 3920

This theorem is referenced by:  ssrexf  4002  nfpw  4575  ssiun2s  5006  triun  5221  iunopeqop  5477  ssopab2bw  5503  ssopab2b  5505  nffr  5605  nfrel  5737  nffun  6523  nff  6666  fvmptss  6962  ssoprab2b  7437  eqoprab2bw  7438  tfis  7807  ovmptss  8045  nffrecs  8235  oawordeulem  8491  nnawordex  8575  r1val1  9710  cardaleph  10011  nfsum1  15625  nfsum  15626  nfcprod1  15843  nfcprod  15844  iunconn  23384  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  ovoliunnul  25476  limciun  25863  ssiun2sf  32645  ssrelf  32704  funimass4f  32726  fsumiunle  32920  prodindf  32954  esumiun  34271  bnj1408  35211  totbndbnd  38037  naddwordnexlem4  43755  ss2iundf  44012  iunconnlem2  45287  iinssdf  45495  rnmptssbi  45615  stoweidlem53  46408  stoweidlem57  46412  meaiunincf  46838  meaiuninc3  46840  opnvonmbllem2  46988  smflim  47132  nfsetrecs  50042  setrec2fun  50048