Theorem nfin 4160

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

Syntax hints:   ∈ wcel 2105  Ⅎwnfc 2884  {crab 3403   ∩ cin 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-rab 3404  df-in 3903

This theorem is referenced by:  csbin  4383  iunxdif3  5036  disjxun  5084  nfres  5912  nfpred  6229  cp  9726  tskwe  9785  iunconn  22659  ptclsg  22846  restmetu  23806  limciun  25138  disjunsn  31064  ordtconnlem1  32010  esum2d  32197  finminlem  34577  bj-rcleqf  35283  mbfposadd  35901  iunconnlem2  42794  inn0f  42860  disjrnmpt2  42972  disjinfi  42977  fsumiunss  43371  stoweidlem57  43853  fourierdlem80  43982  sge0iunmptlemre  44209  iundjiun  44254  pimiooltgt  44504  smflim  44571  smfpimcclem  44601  smfpimcc  44602  adddmmbl  44627  adddmmbl2  44628  muldmmbl  44629  muldmmbl2  44630  smfdivdmmbl2  44635