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

Theorem nfss 3326
Description: If is not free in and , it is not free in . (Contributed by NM, 27-Dec-1996.)
Hypotheses
Ref Expression
dfss2f.1
dfss2f.2
Assertion
Ref Expression
nfss

Proof of Theorem nfss
StepHypRef Expression
1 dfss2f.1 . . 3
2 dfss2f.2 . . 3
31, 2dfss3f 3325 . 2
4 nfra1 2745 . 2
53, 4nfxfr 1610 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1584  e.wcel 1749  F/_wnfc 2545  A.wral 2694  C_wss 3305
This theorem is referenced by:  nfpw  3849  ssiun2s  4189  triun  4373  ssopab2b  4588  nffr  4665  nfrel  4896  nffun  5412  nff  5525  fvmptss  5752  ssoprab2b  6113  tfis  6435  ovmptss  6623  oawordeulem  6954  nnawordex  7037  r1val1  7940  cardaleph  8206  nfsum1  13108  nfsum  13109  iuncon  18736  ovolfiniun  20684  ovoliunlem3  20687  ovoliun  20688  ovoliun2  20689  ovoliunnul  20690  limciun  21069  ssiun2sf  25590  ssrelf  25625  funimass4f  25631  nfcprod1  27125  nfcprod  27126  nfwrecs  27421  totbndbnd  28359  ssrexf  29408  stoweidlem53  29522  stoweidlem57  29526  iunconlem2  31249  bnj1408  31605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ral 2699  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator