Theorem nfss 3927

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

Syntax hints:  Ⅎwnf 1802   ∈ wcel 2141  Ⅎwnfc 2908  ∀wral 3075   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-10 2174  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-clel 2836  df-nfc 2910  df-ral 3076  df-ss 3919

This theorem is referenced by:  ssrexf  4001  nfpw  4571  ssiun2s  5003  triun  5219  iunopeqop  5487  iunopeqopOLD  5488  ssopab2bw  5514  ssopab2b  5516  nffr  5616  nfrel  5748  nffun  6539  nff  6682  fvmptss  6983  ssoprab2b  7460  eqoprab2bw  7461  tfis  7830  ovmptss  8066  nffrecs  8258  oawordeulem  8517  nnawordex  8601  r1val1  9738  cardaleph  10039  nfsum1  15708  nfsum  15709  nfcprod1  15929  nfcprod  15930  iunconn  23476  ovolfiniun  25551  ovoliunlem3  25554  ovoliun  25555  ovoliun2  25556  ovoliunnul  25557  limciun  25944  ssiun2sf  32719  ssrelf  32778  funimass4f  32800  fsumiunle  32992  prodindf  33001  esumiun  34352  bnj1408  35292  totbndbnd  38249  naddwordnexlem4  43939  ss2iundf  44196  iunconnlem2  45471  iinssdf  45678  rnmptssbi  45796  stoweidlem53  46588  stoweidlem57  46592  meaiunincf  47018  meaiuninc3  47020  opnvonmbllem2  47168  smflim  47312  nfsetrecs  50268  setrec2fun  50274