Theorem nfss 3339

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 3338	. 2 |- ( A C_ B <-> A. x e. A x e. B )
4		nfra1 2758	. 2 |- F/ x A. x e. A x e. B
5	3, 4	nfxfr 1620	1 |- F/ x A C_ B

Syntax hints:   F/wnf 1594   e. wcel 1757   F/_wnfc 2558   A.wral 2707   C_ wss 3318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2712  df-in 3325  df-ss 3332

This theorem is referenced by:  nfpw  3862  ssiun2s  4204  triun  4388  ssopab2b  4606  nffr  4683  nfrel  4914  nffun  5430  nff  5545  fvmptss  5772  ssoprab2b  6134  tfis  6456  ovmptss  6645  oawordeulem  6983  nnawordex  7066  r1val1  7983  cardaleph  8249  nfsum1  13153  nfsum  13154  iuncon  18876  ovolfiniun  20828  ovoliunlem3  20831  ovoliun  20832  ovoliun2  20833  ovoliunnul  20834  limciun  21213  ssiun2sf  25736  ssrelf  25771  funimass4f  25777  nfcprod1  27272  nfcprod  27273  nfwrecs  27568  totbndbnd  28534  ssrexf  29582  stoweidlem53  29696  stoweidlem57  29700  iunconlem2  31413  bnj1408  31769