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

Theorem nfss 3561
 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 3560 . 2 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 nfra1 2925 . 2 𝑥𝑥𝐴 𝑥𝐵
53, 4nfxfr 1771 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738  ∀wral 2896   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-in 3547  df-ss 3554 This theorem is referenced by:  ssrexf  3628  nfpw  4120  ssiun2s  4500  triun  4694  iunopeqop  4906  ssopab2b  4927  nffr  5012  nfrel  5127  nffun  5826  nff  5954  fvmptss  6201  ssoprab2b  6610  tfis  6946  ovmptss  7145  nfwrecs  7296  oawordeulem  7521  nnawordex  7604  r1val1  8532  cardaleph  8795  nfsum1  14268  nfsum  14269  nfcprod1  14479  nfcprod  14480  iuncon  21041  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  limciun  23464  ssiun2sf  28760  ssrelf  28805  funimass4f  28818  esumiun  29483  bnj1408  30358  totbndbnd  32758  ss2iundf  36970  iunconlem2  38193  stoweidlem53  38946  stoweidlem57  38950  opnvonmbllem2  39523  smflim  39663  nfsetrecs  42232  setrec2fun  42238
 Copyright terms: Public domain W3C validator