Theorem nfin 4215

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 3955	. 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 3946

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 3954

This theorem is referenced by:  csbin  4438  iunxdif3  5097  disjxun  5145  nfres  5982  nfpred  6304  cp  9888  tskwe  9947  iunconn  23152  ptclsg  23339  restmetu  24299  limciun  25643  disjunsn  32092  ordtconnlem1  33202  esum2d  33389  finminlem  35506  bj-rcleqf  36209  mbfposadd  36838  iunconnlem2  43998  inn0f  44061  disjrnmpt2  44185  disjinfi  44189  fsumiunss  44589  stoweidlem57  45071  fourierdlem80  45200  sge0iunmptlemre  45429  iundjiun  45474  pimiooltgt  45724  smflim  45791  smfpimcclem  45821  smfpimcc  45822  adddmmbl  45847  adddmmbl2  45848  muldmmbl  45849  muldmmbl2  45850  smfdivdmmbl2  45855