Theorem nfin 3853

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 3615	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
2		nfin.2	. . . 4 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2787	. . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4		nfin.1	. . 3 ⊢ Ⅎ𝑥𝐴
5	3, 4	nfrab 3153	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
6	1, 5	nfcxfr 2791	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∈ wcel 2030  Ⅎwnfc 2780  {crab 2945   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-in 3614

This theorem is referenced by:  csbin  4043  iunxdif3  4638  disjxun  4683  nfres  5430  nfpred  5723  cp  8792  tskwe  8814  iunconn  21279  ptclsg  21466  restmetu  22422  limciun  23703  disjunsn  29533  ordtconnlem1  30098  esum2d  30283  finminlem  32437  mbfposadd  33587  csbingOLD  39369  iunconnlem2  39485  inn0f  39556  disjrnmpt2  39689  disjinfi  39694  fsumiunss  40125  stoweidlem57  40592  fourierdlem80  40721  sge0iunmptlemre  40950  iundjiun  40995  pimiooltgt  41242  smflim  41306  smfpimcclem  41334  smfpimcc  41335