Theorem nfss 3938

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

Syntax hints:  Ⅎwnf 1810   ∈ wcel 2149  Ⅎwnfc 2916  ∀wral 3085   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-clel 2844  df-nfc 2918  df-ral 3086  df-ss 3930

This theorem is referenced by:  ssrexf  4012  nfpw  4583  ssiun2s  5014  triun  5234  iunopeqop  5502  iunopeqopOLD  5503  ssopab2bw  5530  ssopab2b  5532  nffr  5632  nfrel  5764  nffun  6556  nff  6699  fvmptss  7000  ssoprab2b  7477  eqoprab2bw  7478  tfis  7847  ovmptss  8084  nffrecs  8276  oawordeulem  8535  nnawordex  8619  r1val1  9754  cardaleph  10069  nfsum1  15737  nfsum  15738  nfcprod1  15958  nfcprod  15959  iunconn  23550  ovolfiniun  25625  ovoliunlem3  25628  ovoliun  25629  ovoliun2  25630  ovoliunnul  25631  limciun  26018  ssiun2sf  32841  ssrelf  32897  funimass4f  32919  fsumiunle  33110  prodindf  33119  esumiun  34425  bnj1408  35365  totbndbnd  38323  naddwordnexlem4  44013  ss2iundf  44270  iunconnlem2  45528  iinssdf  45742  rnmptssbi  45860  stoweidlem53  46652  stoweidlem57  46656  meaiunincf  47082  meaiuninc3  47084  opnvonmbllem2  47232  smflim  47376  nfsetrecs  50342  setrec2fun  50348