Theorem nfss 3482

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

Syntax hints:   F/wnf 1621   e. wcel 1823   F/_wnfc 2602   A.wral 2804   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-in 3468  df-ss 3475

This theorem is referenced by:  ssrexf  3549  nfpw  4011  ssiun2s  4359  triun  4545  ssopab2b  4763  nffr  4842  nfrel  5076  nffun  5592  nff  5709  fvmptss  5940  ssoprab2b  6327  tfis  6662  ovmptss  6854  oawordeulem  7195  nnawordex  7278  r1val1  8195  cardaleph  8461  nfsum1  13597  nfsum  13598  nfcprod1  13802  nfcprod  13803  iuncon  20098  ovolfiniun  22081  ovoliunlem3  22084  ovoliun  22085  ovoliun2  22086  ovoliunnul  22087  limciun  22467  ssiun2sf  27639  ssrelf  27684  funimass4f  27698  esumiun  28326  nfwrecs  29581  totbndbnd  30528  stoweidlem53  32077  stoweidlem57  32081  iunconlem2  34155  bnj1408  34512