Theorem nfss 3939

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876  ∀wral 3044   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-ss 3931

This theorem is referenced by:  ssrexf  4013  nfpw  4582  ssiun2s  5012  triun  5229  iunopeqop  5481  ssopab2bw  5507  ssopab2b  5509  nffr  5611  nfrel  5742  nffun  6539  nff  6684  fvmptss  6980  ssoprab2b  7458  eqoprab2bw  7459  tfis  7831  ovmptss  8072  nffrecs  8262  oawordeulem  8518  nnawordex  8601  r1val1  9739  cardaleph  10042  nfsum1  15656  nfsum  15657  nfcprod1  15874  nfcprod  15875  iunconn  23315  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  limciun  25795  ssiun2sf  32488  ssrelf  32543  funimass4f  32561  fsumiunle  32754  prodindf  32786  esumiun  34084  bnj1408  35026  totbndbnd  37783  naddwordnexlem4  43390  ss2iundf  43648  iunconnlem2  44924  iinssdf  45133  rnmptssbi  45254  stoweidlem53  46051  stoweidlem57  46055  meaiunincf  46481  meaiuninc3  46483  opnvonmbllem2  46631  smflim  46775  nfsetrecs  49675  setrec2fun  49681