Theorem nfin 4143

Description: Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)

Hypotheses

Ref	Expression
nfin.1	⊢ Ⅎ𝑥𝐴
nfin.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfin	⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Proof of Theorem nfin

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfin5 3889	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
2		nfin.2	. . . 4 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2943	. . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4		nfin.1	. . 3 ⊢ Ⅎ𝑥𝐴
5	3, 4	nfrabw 3338	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
6	1, 5	nfcxfr 2953	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∈ wcel 2111  Ⅎwnfc 2936  {crab 3110   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-in 3888

This theorem is referenced by:  csbin  4347  iunxdif3  4980  disjxun  5028  nfres  5820  nfpred  6121  cp  9304  tskwe  9363  iunconn  22033  ptclsg  22220  restmetu  23177  limciun  24497  disjunsn  30357  ordtconnlem1  31277  esum2d  31462  finminlem  33779  bj-rcleqf  34461  mbfposadd  35104  iunconnlem2  41641  inn0f  41707  disjrnmpt2  41815  disjinfi  41820  fsumiunss  42217  stoweidlem57  42699  fourierdlem80  42828  sge0iunmptlemre  43054  iundjiun  43099  pimiooltgt  43346  smflim  43410  smfpimcclem  43438  smfpimcc  43439