Theorem nfss 3596

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

Syntax hints:   F/wnf 1708   e. wcel 1990   F/_wnfc 2751   A.wral 2912   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-in 3581  df-ss 3588

This theorem is referenced by:  ssrexf  3665  nfpw  4172  ssiun2s  4564  triun  4766  iunopeqop  4981  ssopab2b  5002  nffr  5088  nfrel  5204  nffun  5911  nff  6041  fvmptss  6292  ssoprab2b  6712  tfis  7054  ovmptss  7258  nfwrecs  7409  oawordeulem  7634  nnawordex  7717  r1val1  8649  cardaleph  8912  nfsum1  14420  nfsum  14421  nfcprod1  14640  nfcprod  14641  iunconn  21231  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  ovoliunnul  23275  limciun  23658  ssiun2sf  29378  ssrelf  29425  funimass4f  29437  fsumiunle  29575  prodindf  30085  esumiun  30156  bnj1408  31104  totbndbnd  33588  ss2iundf  37951  iunconnlem2  39171  iinssdf  39328  rnmptssbi  39477  stoweidlem53  40270  stoweidlem57  40274  opnvonmbllem2  40847  smflim  40985  nfsetrecs  42433  setrec2fun  42439