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