Theorem nfss 3908

Description: If 𝑥 is not free in 𝐴 and 𝐵, it is not free in 𝐴 ⊆ 𝐵. (Contributed by NM, 27-Dec-1996.)

Hypotheses

Ref	Expression
dfssf.1	⊢ Ⅎ𝑥𝐴
dfssf.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfss	⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Proof of Theorem nfss

Step	Hyp	Ref	Expression
1		dfssf.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfssf.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss3f 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
4		nfra1 3263	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
5	3, 4	nfxfr 1860	1 ⊢ Ⅎ𝑥 𝐴 ⊆ 𝐵

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2119  Ⅎwnfc 2886  ∀wral 3053   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-clel 2814  df-nfc 2888  df-ral 3054  df-ss 3900

This theorem is referenced by:  ssrexf  3981  nfpw  4548  ssiun2s  4978  triun  5194  iunopeqop  5462  iunopeqopOLD  5463  ssopab2bw  5489  ssopab2b  5491  nffr  5591  nfrel  5723  nffun  6508  nff  6651  fvmptss  6948  ssoprab2b  7425  eqoprab2bw  7426  tfis  7795  ovmptss  8032  nffrecs  8223  oawordeulem  8479  nnawordex  8563  r1val1  9701  cardaleph  10002  nfsum1  15643  nfsum  15644  nfcprod1  15864  nfcprod  15865  iunconn  23411  ovolfiniun  25486  ovoliunlem3  25489  ovoliun  25490  ovoliun2  25491  ovoliunnul  25492  limciun  25879  ssiun2sf  32648  ssrelf  32707  funimass4f  32729  fsumiunle  32921  prodindf  32941  esumiun  34278  bnj1408  35218  totbndbnd  38156  naddwordnexlem4  43846  ss2iundf  44103  iunconnlem2  45378  iinssdf  45586  rnmptssbi  45704  stoweidlem53  46496  stoweidlem57  46500  meaiunincf  46926  meaiuninc3  46928  opnvonmbllem2  47076  smflim  47220  nfsetrecs  50176  setrec2fun  50182