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

Theorem nfss 3186
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 3185 . 2  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
4 nfra1 2606 . 2  |-  F/ x A. x  e.  A  x  e.  B
53, 4nfxfr 1560 1  |-  F/ x  A  C_  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1534    e. wcel 1696   F/_wnfc 2419   A.wral 2556    C_ wss 3165
This theorem is referenced by:  nfpw  3649  ssiun2s  3962  triun  4142  ssopab2b  4307  nffr  4383  tfis  4661  nfrel  4790  nffun  5293  nff  5403  fvmptss  5625  ssoprab2b  5921  ovmptss  6216  oawordeulem  6568  nnawordex  6651  r1val1  7474  cardaleph  7732  nfsum1  12179  nfsum  12180  iuncon  17170  ovolfiniun  18876  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  ovoliunnul  18882  limciun  19260  funimass4f  23058  sbcss12g  23157  ssiun2sf  23173  nfcprod1  24132  nfcprod  24133  totbndbnd  26616  ssrexf  27787  stoweidlem53  27905  stoweidlem57  27909  bnj1408  29382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator