Theorem nfss 3936

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876  ∀wral 3044   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-ss 3928

This theorem is referenced by:  ssrexf  4010  nfpw  4578  ssiun2s  5007  triun  5224  iunopeqop  5476  ssopab2bw  5502  ssopab2b  5504  nffr  5604  nfrel  5734  nffun  6523  nff  6666  fvmptss  6962  ssoprab2b  7438  eqoprab2bw  7439  tfis  7811  ovmptss  8049  nffrecs  8239  oawordeulem  8495  nnawordex  8578  r1val1  9715  cardaleph  10018  nfsum1  15632  nfsum  15633  nfcprod1  15850  nfcprod  15851  iunconn  23291  ovolfiniun  25378  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  ovoliunnul  25384  limciun  25771  ssiun2sf  32461  ssrelf  32516  funimass4f  32534  fsumiunle  32727  prodindf  32759  esumiun  34057  bnj1408  34999  totbndbnd  37756  naddwordnexlem4  43363  ss2iundf  43621  iunconnlem2  44897  iinssdf  45106  rnmptssbi  45227  stoweidlem53  46024  stoweidlem57  46028  meaiunincf  46454  meaiuninc3  46456  opnvonmbllem2  46604  smflim  46748  nfsetrecs  49648  setrec2fun  49654