Theorem nfss 3960

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2961  ∀wral 3138   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-in 3943  df-ss 3952

This theorem is referenced by:  ssrexf  4031  nfpw  4560  ssiun2s  4972  triun  5185  iunopeqop  5411  ssopab2bw  5434  ssopab2b  5436  nffr  5529  nfrel  5654  nffun  6378  nff  6510  fvmptss  6780  ssoprab2b  7223  eqoprab2bw  7224  tfis  7569  ovmptss  7788  nfwrecs  7949  oawordeulem  8180  nnawordex  8263  r1val1  9215  cardaleph  9515  nfsum1  15046  nfsumw  15047  nfsum  15048  nfcprod1  15264  nfcprod  15265  iunconn  22036  ovolfiniun  24102  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  ovoliunnul  24108  limciun  24492  ssiun2sf  30311  ssrelf  30366  funimass4f  30382  fsumiunle  30545  prodindf  31282  esumiun  31353  bnj1408  32308  nffrecs  33120  totbndbnd  35082  ss2iundf  40024  iunconnlem2  41289  iinssdf  41428  rnmptssbi  41554  stoweidlem53  42358  stoweidlem57  42362  meaiunincf  42785  meaiuninc3  42787  opnvonmbllem2  42935  smflim  43073  nfsetrecs  44809  setrec2fun  44815