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

Theorem nfss 3936
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 3935 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 3207 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1854 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1785  wcel 2115  wnfc 2958  wral 3126  wss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-v 3473  df-in 3917  df-ss 3927
This theorem is referenced by:  ssrexf  4007  nfpw  4533  ssiun2s  4945  triun  5158  iunopeqop  5384  ssopab2bw  5407  ssopab2b  5409  nffr  5502  nfrel  5627  nffun  6351  nff  6483  fvmptss  6753  ssoprab2b  7197  eqoprab2bw  7198  tfis  7544  ovmptss  7763  nfwrecs  7924  oawordeulem  8155  nnawordex  8238  r1val1  9191  cardaleph  9492  nfsum1  15025  nfsum  15026  nfsumOLD  15027  nfcprod1  15243  nfcprod  15244  iunconn  22011  ovolfiniun  24083  ovoliunlem3  24086  ovoliun  24087  ovoliun2  24088  ovoliunnul  24089  limciun  24475  ssiun2sf  30297  ssrelf  30352  funimass4f  30368  fsumiunle  30531  prodindf  31289  esumiun  31360  bnj1408  32315  nffrecs  33127  totbndbnd  35107  ss2iundf  40141  iunconnlem2  41426  iinssdf  41564  rnmptssbi  41690  stoweidlem53  42488  stoweidlem57  42492  meaiunincf  42915  meaiuninc3  42917  opnvonmbllem2  43065  smflim  43203  nfsetrecs  44978  setrec2fun  44984
  Copyright terms: Public domain W3C validator