Theorem nfss 3930

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

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

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 3922

This theorem is referenced by:  ssrexf  4004  nfpw  4572  ssiun2s  5000  triun  5216  iunopeqop  5468  ssopab2bw  5494  ssopab2b  5496  nffr  5596  nfrel  5727  nffun  6509  nff  6652  fvmptss  6946  ssoprab2b  7422  eqoprab2bw  7423  tfis  7795  ovmptss  8033  nffrecs  8223  oawordeulem  8479  nnawordex  8562  r1val1  9701  cardaleph  10002  nfsum1  15615  nfsum  15616  nfcprod1  15833  nfcprod  15834  iunconn  23331  ovolfiniun  25418  ovoliunlem3  25421  ovoliun  25422  ovoliun2  25423  ovoliunnul  25424  limciun  25811  ssiun2sf  32521  ssrelf  32576  funimass4f  32594  fsumiunle  32787  prodindf  32819  esumiun  34063  bnj1408  35005  totbndbnd  37771  naddwordnexlem4  43377  ss2iundf  43635  iunconnlem2  44911  iinssdf  45120  rnmptssbi  45241  stoweidlem53  46038  stoweidlem57  46042  meaiunincf  46468  meaiuninc3  46470  opnvonmbllem2  46618  smflim  46762  nfsetrecs  49675  setrec2fun  49681