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

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
StepHypRef Expression
1 dfss2f.1 . . 3  |-  F/_ x A
2 dfss2f.2 . . 3  |-  F/_ x B
31, 2dfss3f 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
53, 4nfxfr 1692 1  |-  F/ x  A  C_  B
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator