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

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

Proof of Theorem nfss
StepHypRef Expression
1 dfssf.1 . . 3 𝑥𝐴
2 dfssf.2 . . 3 𝑥𝐵
31, 2dfss3f 3968 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 3271 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1847 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1777  wcel 2098  wnfc 2875  wral 3050  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-10 2129  ax-11 2146  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-clel 2802  df-nfc 2877  df-ral 3051  df-ss 3961
This theorem is referenced by:  ssrexf  4043  nfpw  4623  ssiun2s  5052  triun  5281  iunopeqop  5523  ssopab2bw  5549  ssopab2b  5551  nffr  5652  nfrel  5781  nffun  6577  nff  6719  fvmptss  7016  ssoprab2b  7489  eqoprab2bw  7490  tfis  7860  ovmptss  8098  nffrecs  8289  nfwrecsOLD  8323  oawordeulem  8575  nnawordex  8658  r1val1  9811  cardaleph  10114  nfsum1  15672  nfsum  15673  nfcprod1  15890  nfcprod  15891  iunconn  23376  ovolfiniun  25474  ovoliunlem3  25477  ovoliun  25478  ovoliun2  25479  ovoliunnul  25480  limciun  25867  ssiun2sf  32429  ssrelf  32484  funimass4f  32503  fsumiunle  32677  prodindf  33773  esumiun  33844  bnj1408  34798  totbndbnd  37393  naddwordnexlem4  42973  ss2iundf  43231  iunconnlem2  44516  iinssdf  44645  rnmptssbi  44775  stoweidlem53  45579  stoweidlem57  45583  meaiunincf  46009  meaiuninc3  46011  opnvonmbllem2  46159  smflim  46303  nfsetrecs  48303  setrec2fun  48309
  Copyright terms: Public domain W3C validator