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

Theorem nfss 3173
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 3172 . 2  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
4 nfra1 2593 . 2  |-  F/ x A. x  e.  A  x  e.  B
53, 4nfxfr 1557 1  |-  F/ x  A  C_  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    e. wcel 1684   F/_wnfc 2406   A.wral 2543    C_ wss 3152
This theorem is referenced by:  nfpw  3636  ssiun2s  3946  triun  4126  ssopab2b  4291  nffr  4367  tfis  4645  nfrel  4774  nffun  5277  nff  5387  fvmptss  5609  ssoprab2b  5905  ovmptss  6200  oawordeulem  6552  nnawordex  6635  r1val1  7458  cardaleph  7716  nfsum1  12163  nfsum  12164  iuncon  17154  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  limciun  19244  funimass4f  23042  sbcss12g  23141  ssiun2sf  23157  totbndbnd  26513  ssrexf  27684  stoweidlem53  27802  stoweidlem57  27806  bnj1408  29066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator