Theorem nfss 3956

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2884  ∀wral 3052   ⊆ wss 3931

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 2810  df-nfc 2886  df-ral 3053  df-ss 3948

This theorem is referenced by:  ssrexf  4030  nfpw  4599  ssiun2s  5029  triun  5249  iunopeqop  5501  ssopab2bw  5527  ssopab2b  5529  nffr  5632  nfrel  5763  nffun  6564  nff  6707  fvmptss  7003  ssoprab2b  7481  eqoprab2bw  7482  tfis  7855  ovmptss  8097  nffrecs  8287  nfwrecsOLD  8321  oawordeulem  8571  nnawordex  8654  r1val1  9805  cardaleph  10108  nfsum1  15711  nfsum  15712  nfcprod1  15929  nfcprod  15930  iunconn  23371  ovolfiniun  25459  ovoliunlem3  25462  ovoliun  25463  ovoliun2  25464  ovoliunnul  25465  limciun  25852  ssiun2sf  32545  ssrelf  32600  funimass4f  32620  fsumiunle  32813  prodindf  32845  esumiun  34130  bnj1408  35072  totbndbnd  37818  naddwordnexlem4  43392  ss2iundf  43650  iunconnlem2  44926  iinssdf  45130  rnmptssbi  45251  stoweidlem53  46049  stoweidlem57  46053  meaiunincf  46479  meaiuninc3  46481  opnvonmbllem2  46629  smflim  46773  nfsetrecs  49517  setrec2fun  49523