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

Theorem nfss 3333
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 3332 . 2  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
4 nfra1 2748 . 2  |-  F/ x A. x  e.  A  x  e.  B
53, 4nfxfr 1579 1  |-  F/ x  A  C_  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1553    e. wcel 1725   F/_wnfc 2558   A.wral 2697    C_ wss 3312
This theorem is referenced by:  nfpw  3802  ssiun2s  4127  triun  4307  ssopab2b  4473  nffr  4548  tfis  4826  nfrel  4954  nffun  5468  nff  5581  fvmptss  5805  ssoprab2b  6123  ovmptss  6420  oawordeulem  6789  nnawordex  6872  r1val1  7704  cardaleph  7962  nfsum1  12476  nfsum  12477  iuncon  17483  ovolfiniun  19389  ovoliunlem3  19392  ovoliun  19393  ovoliun2  19394  ovoliunnul  19395  limciun  19773  ssiun2sf  24002  funimass4f  24036  nfcprod1  25228  nfcprod  25229  nfwrecs  25525  totbndbnd  26489  ssrexf  27651  stoweidlem53  27769  stoweidlem57  27773  iunconlem2  28984  bnj1408  29342
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator