Theorem nfss 3901

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

This proof depends on syntax axioms:  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907  ∀wral 3076   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-10 2177  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909  df-ral 3077  df-ss 3896

This theorem is used by:  ssrexf  3975  nfpw  4576  ssiun2s  5006  triun  5226  iunopeqop  5493  iunopeqopOLD  5494  ssopab2bw  5521  ssopab2b  5523  nffr  5623  nfrel  5755  nffun  6563  nff  6706  fvmptss  7007  ssoprab2b  7490  eqoprab2bw  7491  tfis  7867  ovmptssOLD  8106  nffrecs  8305  oawordeulem  8566  nnawordex  8650  r1val1  9797  setrec2fun  9977  cardaleph  10172  nfsum1  15863  nfsum  15864  nfcprod1  16083  nfcprod  16084  iunconn  23752  ovolfiniun  25828  ovoliunlem3  25831  ovoliun  25832  ovoliun2  25833  ovoliunnul  25834  limciun  26220  ssiun2sf  33202  ssrelf  33257  funimass4f  33279  fsumiunle  33467  prodindf  33476  esumiun  34773  bnj1408  35713  totbndbnd  38817  naddwordnexlem4  44497  ss2iundf  44753  iunconnlem2  46011  iinssdf  46248  rnmptssbi  46366  stoweidlem53  47157  stoweidlem57  47161  meaiunincf  47587  meaiuninc3  47589  opnvonmbllem2  47737  smflim  47881  nfsetrecs  50958