Theorem nfss 3936

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

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

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 3928

This theorem is referenced by:  ssrexf  4010  nfpw  4584  ssiun2s  5015  triun  5235  iunopeqop  5505  iunopeqopOLD  5506  ssopab2bw  5533  ssopab2b  5535  nffr  5635  nfrel  5767  nffun  6560  nff  6702  fvmptss  7003  ssoprab2b  7480  eqoprab2bw  7481  tfis  7851  ovmptss  8088  nffrecs  8280  oawordeulem  8539  nnawordex  8623  r1val1  9758  cardaleph  10073  nfsum1  15741  nfsum  15742  nfcprod1  15962  nfcprod  15963  iunconn  23554  ovolfiniun  25629  ovoliunlem3  25632  ovoliun  25633  ovoliun2  25634  ovoliunnul  25635  limciun  26022  ssiun2sf  32845  ssrelf  32901  funimass4f  32923  fsumiunle  33114  prodindf  33123  esumiun  34429  bnj1408  35369  totbndbnd  38363  naddwordnexlem4  44055  ss2iundf  44312  iunconnlem2  45570  iinssdf  45784  rnmptssbi  45902  stoweidlem53  46694  stoweidlem57  46698  meaiunincf  47124  meaiuninc3  47126  opnvonmbllem2  47274  smflim  47418  nfsetrecs  50384  setrec2fun  50390