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

Theorem nfss 3976
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 3975 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 3284 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1853 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1783  wcel 2108  wnfc 2890  wral 3061  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-ss 3968
This theorem is referenced by:  ssrexf  4050  nfpw  4619  ssiun2s  5048  triun  5274  iunopeqop  5526  ssopab2bw  5552  ssopab2b  5554  nffr  5658  nfrel  5789  nffun  6589  nff  6732  fvmptss  7028  ssoprab2b  7502  eqoprab2bw  7503  tfis  7876  ovmptss  8118  nffrecs  8308  nfwrecsOLD  8342  oawordeulem  8592  nnawordex  8675  r1val1  9826  cardaleph  10129  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  iunconn  23436  ovolfiniun  25536  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  ovoliunnul  25542  limciun  25929  ssiun2sf  32572  ssrelf  32627  funimass4f  32647  fsumiunle  32831  prodindf  32848  esumiun  34095  bnj1408  35050  totbndbnd  37796  naddwordnexlem4  43414  ss2iundf  43672  iunconnlem2  44955  iinssdf  45144  rnmptssbi  45267  stoweidlem53  46068  stoweidlem57  46072  meaiunincf  46498  meaiuninc3  46500  opnvonmbllem2  46648  smflim  46792  nfsetrecs  49205  setrec2fun  49211
  Copyright terms: Public domain W3C validator