Theorem nfss 3988

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

Syntax hints:  Ⅎwnf 1780   ∈ wcel 2106  Ⅎwnfc 2888  ∀wral 3059   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-10 2139  ax-11 2155  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-clel 2814  df-nfc 2890  df-ral 3060  df-ss 3980

This theorem is referenced by:  ssrexf  4062  nfpw  4624  ssiun2s  5053  triun  5280  iunopeqop  5531  ssopab2bw  5557  ssopab2b  5559  nffr  5662  nfrel  5792  nffun  6591  nff  6733  fvmptss  7028  ssoprab2b  7502  eqoprab2bw  7503  tfis  7876  ovmptss  8117  nffrecs  8307  nfwrecsOLD  8341  oawordeulem  8591  nnawordex  8674  r1val1  9824  cardaleph  10127  nfsum1  15723  nfsum  15724  nfcprod1  15941  nfcprod  15942  iunconn  23452  ovolfiniun  25550  ovoliunlem3  25553  ovoliun  25554  ovoliun2  25555  ovoliunnul  25556  limciun  25944  ssiun2sf  32580  ssrelf  32635  funimass4f  32654  fsumiunle  32836  prodindf  34004  esumiun  34075  bnj1408  35029  totbndbnd  37776  naddwordnexlem4  43391  ss2iundf  43649  iunconnlem2  44933  iinssdf  45079  rnmptssbi  45206  stoweidlem53  46009  stoweidlem57  46013  meaiunincf  46439  meaiuninc3  46441  opnvonmbllem2  46589  smflim  46733  nfsetrecs  48917  setrec2fun  48923