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

Theorem nfss 3482
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 3481 . 2  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
4 nfra1 2835 . 2  |-  F/ x A. x  e.  A  x  e.  B
53, 4nfxfr 1650 1  |-  F/ x  A  C_  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1621    e. wcel 1823   F/_wnfc 2602   A.wral 2804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-in 3468  df-ss 3475
This theorem is referenced by:  ssrexf  3549  nfpw  4011  ssiun2s  4359  triun  4545  ssopab2b  4763  nffr  4842  nfrel  5076  nffun  5592  nff  5709  fvmptss  5940  ssoprab2b  6327  tfis  6662  ovmptss  6854  oawordeulem  7195  nnawordex  7278  r1val1  8195  cardaleph  8461  nfsum1  13597  nfsum  13598  nfcprod1  13802  nfcprod  13803  iuncon  20098  ovolfiniun  22081  ovoliunlem3  22084  ovoliun  22085  ovoliun2  22086  ovoliunnul  22087  limciun  22467  ssiun2sf  27639  ssrelf  27684  funimass4f  27698  esumiun  28326  nfwrecs  29581  totbndbnd  30528  stoweidlem53  32077  stoweidlem57  32081  iunconlem2  34155  bnj1408  34512
  Copyright terms: Public domain W3C validator