Theorem nfss 3436

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

Syntax hints:   F/wnf 1677   e. wcel 1897   F/_wnfc 2589   A.wral 2748   C_ wss 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-in 3422  df-ss 3429

This theorem is referenced by:  ssrexf  3503  nfpw  3974  ssiun2s  4335  triun  4523  ssopab2b  4741  nffr  4826  nfrel  4938  nffun  5622  nff  5746  fvmptss  5980  ssoprab2b  6374  tfis  6707  ovmptss  6903  nfwrecs  7055  oawordeulem  7280  nnawordex  7363  r1val1  8282  cardaleph  8545  nfsum1  13804  nfsum  13805  nfcprod1  14012  nfcprod  14013  iuncon  20491  ovolfiniun  22502  ovoliunlem3  22505  ovoliun  22506  ovoliun2  22507  ovoliunnul  22508  limciun  22897  ssiun2sf  28222  ssrelf  28269  funimass4f  28282  esumiun  28963  bnj1408  29893  totbndbnd  32165  ss2iundf  36295  iunconlem2  37371  stoweidlem53  37951  stoweidlem57  37955  opnvonmbllem2  38492  iunopeqop  39044