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

Theorem nfss 3555
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 3554 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 2919 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1769 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1698  wcel 1975  wnfc 2732  wral 2890  wss 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ral 2895  df-in 3541  df-ss 3548
This theorem is referenced by:  ssrexf  3622  nfpw  4114  ssiun2s  4489  triun  4683  ssopab2b  4912  nffr  4997  nfrel  5112  nffun  5807  nff  5935  fvmptss  6181  ssoprab2b  6583  tfis  6918  ovmptss  7117  nfwrecs  7268  oawordeulem  7493  nnawordex  7576  r1val1  8504  cardaleph  8767  nfsum1  14209  nfsum  14210  nfcprod1  14420  nfcprod  14421  iuncon  20978  ovolfiniun  22988  ovoliunlem3  22991  ovoliun  22992  ovoliun2  22993  ovoliunnul  22994  limciun  23376  ssiun2sf  28561  ssrelf  28606  funimass4f  28619  esumiun  29284  bnj1408  30159  totbndbnd  32556  ss2iundf  36768  iunconlem2  37991  stoweidlem53  38745  stoweidlem57  38749  opnvonmbllem2  39322  smflim  39462  iunopeqop  40126
  Copyright terms: Public domain W3C validator