Theorem nfss 3909

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 3908	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3142	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1856	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886  ∀wral 3063   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssrexf  3981  nfpw  4551  ssiun2s  4974  triun  5200  iunopeqop  5429  ssopab2bw  5453  ssopab2b  5455  nffr  5554  nfrel  5680  nffun  6441  nff  6580  fvmptss  6869  ssoprab2b  7322  eqoprab2bw  7323  tfis  7676  ovmptss  7904  nffrecs  8070  nfwrecsOLD  8104  oawordeulem  8347  nnawordex  8430  r1val1  9475  cardaleph  9776  nfsum1  15329  nfsum  15330  nfsumOLD  15331  nfcprod1  15548  nfcprod  15549  iunconn  22487  ovolfiniun  24570  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  ovoliunnul  24576  limciun  24963  ssiun2sf  30800  ssrelf  30856  funimass4f  30873  fsumiunle  31045  prodindf  31891  esumiun  31962  bnj1408  32916  totbndbnd  35874  ss2iundf  41156  iunconnlem2  42444  iinssdf  42577  rnmptssbi  42696  stoweidlem53  43484  stoweidlem57  43488  meaiunincf  43911  meaiuninc3  43913  opnvonmbllem2  44061  smflim  44199  nfsetrecs  46278  setrec2fun  46284