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

Theorem nfss 3588
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 3587 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 2938 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1777 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1706  wcel 1988  wnfc 2749  wral 2909  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-in 3574  df-ss 3581
This theorem is referenced by:  ssrexf  3657  nfpw  4163  ssiun2s  4555  triun  4757  iunopeqop  4971  ssopab2b  4992  nffr  5078  nfrel  5194  nffun  5899  nff  6028  fvmptss  6279  ssoprab2b  6697  tfis  7039  ovmptss  7243  nfwrecs  7394  oawordeulem  7619  nnawordex  7702  r1val1  8634  cardaleph  8897  nfsum1  14401  nfsum  14402  nfcprod1  14621  nfcprod  14622  iunconn  21212  ovolfiniun  23250  ovoliunlem3  23253  ovoliun  23254  ovoliun2  23255  ovoliunnul  23256  limciun  23639  ssiun2sf  29350  ssrelf  29397  funimass4f  29410  fsumiunle  29549  prodindf  30059  esumiun  30130  bnj1408  31078  totbndbnd  33559  ss2iundf  37770  iunconnlem2  38991  iinssdf  39148  rnmptssbi  39293  stoweidlem53  40033  stoweidlem57  40037  opnvonmbllem2  40610  smflim  40748  nfsetrecs  42198  setrec2fun  42204
  Copyright terms: Public domain W3C validator