MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfss Unicode version

Theorem nfss 3284
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
StepHypRef Expression
1 dfss2f.1 . . 3  |-  F/_ x A
2 dfss2f.2 . . 3  |-  F/_ x B
31, 2dfss3f 3283 . 2  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
4 nfra1 2699 . 2  |-  F/ x A. x  e.  A  x  e.  B
53, 4nfxfr 1576 1  |-  F/ x  A  C_  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    e. wcel 1717   F/_wnfc 2510   A.wral 2649    C_ wss 3263
This theorem is referenced by:  nfpw  3753  ssiun2s  4076  triun  4256  ssopab2b  4422  nffr  4497  tfis  4774  nfrel  4902  nffun  5416  nff  5529  fvmptss  5752  ssoprab2b  6070  ovmptss  6367  oawordeulem  6733  nnawordex  6816  r1val1  7645  cardaleph  7903  nfsum1  12411  nfsum  12412  iuncon  17412  ovolfiniun  19264  ovoliunlem3  19267  ovoliun  19268  ovoliun2  19269  ovoliunnul  19270  limciun  19648  ssiun2sf  23854  funimass4f  23887  nfcprod1  25015  nfcprod  25016  totbndbnd  26189  ssrexf  27352  stoweidlem53  27470  stoweidlem57  27474  bnj1408  28743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator