Theorem nfss 3913

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887  ∀wral 3064   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ssrexf  3985  nfpw  4554  ssiun2s  4978  triun  5204  iunopeqop  5435  ssopab2bw  5460  ssopab2b  5462  nffr  5563  nfrel  5690  nffun  6457  nff  6596  fvmptss  6887  ssoprab2b  7344  eqoprab2bw  7345  tfis  7701  ovmptss  7933  nffrecs  8099  nfwrecsOLD  8133  oawordeulem  8385  nnawordex  8468  r1val1  9544  cardaleph  9845  nfsum1  15401  nfsum  15402  nfsumOLD  15403  nfcprod1  15620  nfcprod  15621  iunconn  22579  ovolfiniun  24665  ovoliunlem3  24668  ovoliun  24669  ovoliun2  24670  ovoliunnul  24671  limciun  25058  ssiun2sf  30899  ssrelf  30955  funimass4f  30972  fsumiunle  31143  prodindf  31991  esumiun  32062  bnj1408  33016  totbndbnd  35947  ss2iundf  41267  iunconnlem2  42555  iinssdf  42688  rnmptssbi  42807  stoweidlem53  43594  stoweidlem57  43598  meaiunincf  44021  meaiuninc3  44023  opnvonmbllem2  44171  smflim  44312  nfsetrecs  46392  setrec2fun  46398