Theorem nfss 3974

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

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfss2f.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss3f 3973	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3281	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1855	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2883  ∀wral 3061   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ssrexf  4048  nfpw  4621  ssiun2s  5051  triun  5280  iunopeqop  5521  ssopab2bw  5547  ssopab2b  5549  nffr  5650  nfrel  5779  nffun  6571  nff  6713  fvmptss  7010  ssoprab2b  7477  eqoprab2bw  7478  tfis  7843  ovmptss  8078  nffrecs  8267  nfwrecsOLD  8301  oawordeulem  8553  nnawordex  8636  r1val1  9780  cardaleph  10083  nfsum1  15635  nfsum  15636  nfcprod1  15853  nfcprod  15854  iunconn  22931  ovolfiniun  25017  ovoliunlem3  25020  ovoliun  25021  ovoliun2  25022  ovoliunnul  25023  limciun  25410  ssiun2sf  31786  ssrelf  31839  funimass4f  31856  fsumiunle  32030  prodindf  33016  esumiun  33087  bnj1408  34042  totbndbnd  36652  naddwordnexlem4  42142  ss2iundf  42400  iunconnlem2  43686  iinssdf  43818  rnmptssbi  43955  stoweidlem53  44759  stoweidlem57  44763  meaiunincf  45189  meaiuninc3  45191  opnvonmbllem2  45339  smflim  45483  nfsetrecs  47721  setrec2fun  47727