Theorem nfin 3803

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

Syntax hints:   ∈ wcel 1992  Ⅎwnfc 2754  {crab 2916   ∩ cin 3559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-in 3567

This theorem is referenced by:  csbin  3987  iunxdif3  4577  disjxun  4616  nfres  5362  nfpred  5647  cp  8699  tskwe  8721  iunconn  21136  ptclsg  21323  restmetu  22280  limciun  23559  disjunsn  29243  ordtconnlem1  29744  esum2d  29928  finminlem  31927  mbfposadd  33056  csbingOLD  38504  iunconnlem2  38621  inn0f  38694  disjrnmpt2  38816  disjinfi  38821  fsumiunss  39179  stoweidlem57  39549  fourierdlem80  39678  sge0iunmptlemre  39907  iundjiun  39952  pimiooltgt  40196  smflim  40260  smfpimcclem  40288  smfpimcc  40289