Theorem nfss 3906

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911  ∀wral 3080   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-clel 2839  df-nfc 2913  df-ral 3081  df-ss 3901

This theorem is used by:  ssrexf  3980  nfpw  4580  ssiun2s  5012  triun  5233  iunopeqop  5501  iunopeqopOLD  5502  ssopab2bw  5529  ssopab2b  5531  nffr  5631  nfrel  5764  nffun  6590  nff  6735  fvmptss  7037  ssoprab2b  7520  eqoprab2bw  7521  tfis  7900  ovmptssOLD  8140  nffrecs  8339  oawordeulem  8600  nnawordex  8684  r1val1  9830  setrec2fun  10010  cardaleph  10207  nfsum1  15901  nfsum  15902  nfcprod1  16121  nfcprod  16122  iunconn  23801  ovolfiniun  25877  ovoliunlem3  25880  ovoliun  25881  ovoliun2  25882  ovoliunnul  25883  limciun  26269  ssiun2sf  33252  ssrelf  33307  funimass4f  33329  fsumiunle  33516  prodindf  33525  esumiun  34837  bnj1408  35777  totbndbnd  38989  naddwordnexlem4  44664  ss2iundf  44920  iunconnlem2  46177  iinssdf  46427  rnmptssbi  46545  stoweidlem53  47336  stoweidlem57  47340  meaiunincf  47766  meaiuninc3  47768  opnvonmbllem2  47916  smflim  48060  nfsetrecs  51195