Theorem nfin 4041

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

Syntax hints:   ∈ wcel 2107  Ⅎwnfc 2919  {crab 3094   ∩ cin 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799

This theorem is referenced by:  csbin  4236  iunxdif3  4840  disjxun  4884  nfres  5644  nfpred  5938  cp  9051  tskwe  9109  iunconn  21640  ptclsg  21827  restmetu  22783  limciun  24095  disjunsn  29970  ordtconnlem1  30568  esum2d  30753  finminlem  32901  mbfposadd  34084  iunconnlem2  40108  inn0f  40177  disjrnmpt2  40302  disjinfi  40307  fsumiunss  40719  stoweidlem57  41205  fourierdlem80  41334  sge0iunmptlemre  41560  iundjiun  41605  pimiooltgt  41852  smflim  41916  smfpimcclem  41944  smfpimcc  41945