Theorem nfin 4217

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

Syntax hints:   ∈ wcel 2104  Ⅎwnfc 2881  {crab 3430   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431  df-in 3956

This theorem is referenced by:  csbin  4440  iunxdif3  5099  disjxun  5147  nfres  5984  nfpred  6306  cp  9890  tskwe  9949  iunconn  23154  ptclsg  23341  restmetu  24301  limciun  25645  disjunsn  32090  ordtconnlem1  33200  esum2d  33387  finminlem  35508  bj-rcleqf  36211  mbfposadd  36840  iunconnlem2  44000  inn0f  44063  disjrnmpt2  44187  disjinfi  44191  fsumiunss  44591  stoweidlem57  45073  fourierdlem80  45202  sge0iunmptlemre  45431  iundjiun  45476  pimiooltgt  45726  smflim  45793  smfpimcclem  45823  smfpimcc  45824  adddmmbl  45849  adddmmbl2  45850  muldmmbl  45851  muldmmbl2  45852  smfdivdmmbl2  45857