Theorem nfss 3923

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2880  ∀wral 3048   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-10 2146  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2808  df-nfc 2882  df-ral 3049  df-ss 3915

This theorem is referenced by:  ssrexf  3997  nfpw  4570  ssiun2s  5001  triun  5216  iunopeqop  5466  ssopab2bw  5492  ssopab2b  5494  nffr  5594  nfrel  5726  nffun  6512  nff  6655  fvmptss  6950  ssoprab2b  7424  eqoprab2bw  7425  tfis  7794  ovmptss  8032  nffrecs  8222  oawordeulem  8478  nnawordex  8561  r1val1  9690  cardaleph  9991  nfsum1  15604  nfsum  15605  nfcprod1  15822  nfcprod  15823  iunconn  23363  ovolfiniun  25449  ovoliunlem3  25452  ovoliun  25453  ovoliun2  25454  ovoliunnul  25455  limciun  25842  ssiun2sf  32560  ssrelf  32619  funimass4f  32641  fsumiunle  32838  prodindf  32872  esumiun  34179  bnj1408  35120  totbndbnd  37902  naddwordnexlem4  43558  ss2iundf  43816  iunconnlem2  45091  iinssdf  45299  rnmptssbi  45420  stoweidlem53  46213  stoweidlem57  46217  meaiunincf  46643  meaiuninc3  46645  opnvonmbllem2  46793  smflim  46937  nfsetrecs  49847  setrec2fun  49853