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

Theorem nfss 3941
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 3940 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 3270 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1856 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1786  wcel 2107  wnfc 2888  wral 3065  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  ssrexf  4013  nfpw  4584  ssiun2s  5013  triun  5242  iunopeqop  5483  ssopab2bw  5509  ssopab2b  5511  nffr  5612  nfrel  5740  nffun  6529  nff  6669  fvmptss  6965  ssoprab2b  7431  eqoprab2bw  7432  tfis  7796  ovmptss  8030  nffrecs  8219  nfwrecsOLD  8253  oawordeulem  8506  nnawordex  8589  r1val1  9729  cardaleph  10032  nfsum1  15581  nfsum  15582  nfsumOLD  15583  nfcprod1  15800  nfcprod  15801  iunconn  22795  ovolfiniun  24881  ovoliunlem3  24884  ovoliun  24885  ovoliun2  24886  ovoliunnul  24887  limciun  25274  ssiun2sf  31520  ssrelf  31576  funimass4f  31593  fsumiunle  31767  prodindf  32662  esumiun  32733  bnj1408  33688  totbndbnd  36277  naddwordnexlem4  41747  ss2iundf  42005  iunconnlem2  43291  iinssdf  43423  rnmptssbi  43563  stoweidlem53  44368  stoweidlem57  44372  meaiunincf  44798  meaiuninc3  44800  opnvonmbllem2  44948  smflim  45092  nfsetrecs  47205  setrec2fun  47211
  Copyright terms: Public domain W3C validator