Theorem nfss 3924

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2907  ∀wral 3076   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2835  df-nfc 2909  df-ral 3077  df-ss 3916

This theorem is used by:  ssrexf  3998  nfpw  4576  ssiun2s  5007  triun  5227  iunopeqop  5498  iunopeqopOLD  5499  ssopab2bw  5526  ssopab2b  5528  nffr  5628  nfrel  5760  nffun  6556  nff  6698  fvmptss  6999  ssoprab2b  7482  eqoprab2bw  7483  tfis  7851  ovmptss  8090  nffrecs  8282  oawordeulem  8541  nnawordex  8625  r1val1  9768  cardaleph  10092  nfsum1  15777  nfsum  15778  nfcprod1  15997  nfcprod  15998  iunconn  23653  ovolfiniun  25729  ovoliunlem3  25732  ovoliun  25733  ovoliun2  25734  ovoliunnul  25735  limciun  26121  ssiun2sf  33033  ssrelf  33088  funimass4f  33110  fsumiunle  33299  prodindf  33308  esumiun  34604  bnj1408  35545  totbndbnd  38539  naddwordnexlem4  44242  ss2iundf  44499  iunconnlem2  45757  iinssdf  45971  rnmptssbi  46089  stoweidlem53  46881  stoweidlem57  46885  meaiunincf  47311  meaiuninc3  47313  opnvonmbllem2  47461  smflim  47605  nfsetrecs  50612  setrec2fun  50618