Theorem nfin 4147

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 3891	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
2		nfin.2	. . . 4 ⊢ Ⅎ𝑥𝐵
3	2	nfcri 2893	. . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
4		nfin.1	. . 3 ⊢ Ⅎ𝑥𝐴
5	3, 4	nfrabw 3311	. 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵}
6	1, 5	nfcxfr 2904	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∈ wcel 2108  Ⅎwnfc 2886  {crab 3067   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-in 3890

This theorem is referenced by:  csbin  4370  iunxdif3  5020  disjxun  5068  nfres  5882  nfpred  6196  cp  9580  tskwe  9639  iunconn  22487  ptclsg  22674  restmetu  23632  limciun  24963  disjunsn  30834  ordtconnlem1  31776  esum2d  31961  finminlem  34434  bj-rcleqf  35142  mbfposadd  35751  iunconnlem2  42444  inn0f  42510  disjrnmpt2  42615  disjinfi  42620  fsumiunss  43006  stoweidlem57  43488  fourierdlem80  43617  sge0iunmptlemre  43843  iundjiun  43888  pimiooltgt  44135  smflim  44199  smfpimcclem  44227  smfpimcc  44228