Theorem nfss 3370

Description: If x is not free in A and B, it is not free in A C_ B. (Contributed by NM, 27-Dec-1996.)

Hypotheses

Ref	Expression
dfss2f.1	|- F/_ x A
dfss2f.2	|- F/_ x B

Assertion

Ref	Expression
nfss	|- F/ x A C_ B

Proof of Theorem nfss

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 |- F/_ x A
2		dfss2f.2	. . 3 |- F/_ x B
3	1, 2	dfss3f 3369	. 2 |- ( A C_ B <-> A. x e. A x e. B )
4		nfra1 2787	. 2 |- F/ x A. x e. A x e. B
5	3, 4	nfxfr 1615	1 |- F/ x A C_ B

Syntax hints:   F/wnf 1589   e. wcel 1756   F/_wnfc 2575   A.wral 2736   C_ wss 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741  df-in 3356  df-ss 3363

This theorem is referenced by:  nfpw  3893  ssiun2s  4235  triun  4419  ssopab2b  4636  nffr  4715  nfrel  4946  nffun  5461  nff  5576  fvmptss  5803  ssoprab2b  6164  tfis  6486  ovmptss  6675  oawordeulem  7014  nnawordex  7097  r1val1  8014  cardaleph  8280  nfsum1  13188  nfsum  13189  iuncon  19054  ovolfiniun  21006  ovoliunlem3  21009  ovoliun  21010  ovoliun2  21011  ovoliunnul  21012  limciun  21391  ssiun2sf  25932  ssrelf  25967  funimass4f  25973  nfcprod1  27445  nfcprod  27446  nfwrecs  27741  totbndbnd  28714  ssrexf  29761  stoweidlem53  29874  stoweidlem57  29878  iunconlem2  31767  bnj1408  32123