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

Theorem nfss 3463
 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 3462 . 2
4 nfra1 2811 . 2
53, 4nfxfr 1616 1
 Colors of variables: wff setvar class Syntax hints:  F/wnf 1590  e.wcel 1758  F/_wnfc 2602  A.wral 2800  C_wss 3442 This theorem is referenced by:  nfpw  3988  ssiun2s  4331  triun  4515  ssopab2b  4732  nffr  4811  nfrel  5042  nffun  5559  nff  5675  fvmptss  5905  ssoprab2b  6275  tfis  6598  ovmptss  6787  oawordeulem  7127  nnawordex  7210  r1val1  8130  cardaleph  8396  nfsum1  13325  nfsum  13326  iuncon  19431  ovolfiniun  21383  ovoliunlem3  21386  ovoliun  21387  ovoliun2  21388  ovoliunnul  21389  limciun  21769  ssiun2sf  26378  ssrelf  26413  funimass4f  26419  nfcprod1  27879  nfcprod  27880  nfwrecs  28175  totbndbnd  29148  ssrexf  30195  stoweidlem53  30582  stoweidlem57  30586  iunconlem2  32514  bnj1408  32870 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2805  df-in 3449  df-ss 3456
 Copyright terms: Public domain W3C validator