Theorem nfss 3457

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

Syntax hints:   F/wnf 1663   e. wcel 1868   F/_wnfc 2570   A.wral 2775   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-in 3443  df-ss 3450

This theorem is referenced by:  ssrexf  3524  nfpw  3991  ssiun2s  4340  triun  4528  ssopab2b  4744  nffr  4824  nfrel  4936  nffun  5620  nff  5739  fvmptss  5971  ssoprab2b  6359  tfis  6692  ovmptss  6885  nfwrecs  7035  oawordeulem  7260  nnawordex  7343  r1val1  8259  cardaleph  8521  nfsum1  13744  nfsum  13745  nfcprod1  13952  nfcprod  13953  iuncon  20430  ovolfiniun  22441  ovoliunlem3  22444  ovoliun  22445  ovoliun2  22446  ovoliunnul  22447  limciun  22836  ssiun2sf  28164  ssrelf  28211  funimass4f  28224  esumiun  28911  bnj1408  29841  totbndbnd  32035  ss2iundf  36111  iunconlem2  37193  stoweidlem53  37734  stoweidlem57  37738  iunopeqop  38707