Theorem nfss 3914

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2883  ∀wral 3051   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-clel 2811  df-nfc 2885  df-ral 3052  df-ss 3906

This theorem is referenced by:  ssrexf  3988  nfpw  4560  ssiun2s  4991  triun  5207  iunopeqop  5475  iunopeqopOLD  5476  ssopab2bw  5502  ssopab2b  5504  nffr  5604  nfrel  5736  nffun  6521  nff  6664  fvmptss  6960  ssoprab2b  7436  eqoprab2bw  7437  tfis  7806  ovmptss  8043  nffrecs  8233  oawordeulem  8489  nnawordex  8573  r1val1  9710  cardaleph  10011  nfsum1  15652  nfsum  15653  nfcprod1  15873  nfcprod  15874  iunconn  23393  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  limciun  25861  ssiun2sf  32629  ssrelf  32688  funimass4f  32710  fsumiunle  32902  prodindf  32922  esumiun  34238  bnj1408  35178  totbndbnd  38110  naddwordnexlem4  43829  ss2iundf  44086  iunconnlem2  45361  iinssdf  45569  rnmptssbi  45689  stoweidlem53  46481  stoweidlem57  46485  meaiunincf  46911  meaiuninc3  46913  opnvonmbllem2  47061  smflim  47205  nfsetrecs  50161  setrec2fun  50167