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

Theorem nfss 3496
 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 3495 . 2
4 nfra1 2838 . 2
53, 4nfxfr 1645 1
 Colors of variables: wff setvar class Syntax hints:  F/wnf 1616  e.wcel 1818  F/_wnfc 2605  A.wral 2807  C_wss 3475 This theorem is referenced by:  nfpw  4024  ssiun2s  4374  triun  4558  ssopab2b  4779  nffr  4858  nfrel  5093  nffun  5615  nff  5732  fvmptss  5964  ssoprab2b  6354  tfis  6689  ovmptss  6881  oawordeulem  7222  nnawordex  7305  r1val1  8225  cardaleph  8491  nfsum1  13512  nfsum  13513  nfcprod1  13717  nfcprod  13718  iuncon  19929  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  limciun  22298  ssiun2sf  27427  ssrelf  27466  funimass4f  27474  nfwrecs  29338  totbndbnd  30285  ssrexf  31388  stoweidlem53  31835  stoweidlem57  31839  iunconlem2  33735  bnj1408  34092 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator