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

Theorem nfss 3629
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 3628 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 2970 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1819 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1748  wcel 2030  wnfc 2780  wral 2941  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-in 3614  df-ss 3621
This theorem is referenced by:  ssrexf  3698  nfpw  4205  ssiun2s  4596  triun  4799  iunopeqop  5010  ssopab2b  5031  nffr  5117  nfrel  5238  nffun  5949  nff  6079  fvmptss  6331  ssoprab2b  6754  tfis  7096  ovmptss  7303  nfwrecs  7454  oawordeulem  7679  nnawordex  7762  r1val1  8687  cardaleph  8950  nfsum1  14464  nfsum  14465  nfcprod1  14684  nfcprod  14685  iunconn  21279  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  ovoliunnul  23321  limciun  23703  ssiun2sf  29504  ssrelf  29553  funimass4f  29565  fsumiunle  29703  prodindf  30213  esumiun  30284  bnj1408  31230  nffrecs  31903  totbndbnd  33718  ss2iundf  38268  iunconnlem2  39485  iinssdf  39642  rnmptssbi  39791  stoweidlem53  40588  stoweidlem57  40592  meaiunincf  41018  meaiuninc3  41020  opnvonmbllem2  41168  smflim  41306  nfsetrecs  42758  setrec2fun  42764
  Copyright terms: Public domain W3C validator