Theorem nfin 4176

Description: Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2146, ax-11 2162, ax-12 2184. (Revised by SN, 14-May-2025.)

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		elin 3917	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2890	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2890	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1900	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1854	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2886	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2113  Ⅎwnfc 2883   ∩ cin 3900

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-v 3442  df-in 3908

This theorem is referenced by:  inn0f  4323  csbin  4394  iunxdif3  5050  disjxun  5096  nfres  5940  nfpred  6264  cp  9803  tskwe  9862  iunconn  23372  ptclsg  23559  restmetu  24514  limciun  25851  disjunsn  32669  ordtconnlem1  34081  esum2d  34250  finminlem  36512  bj-rcleqf  37226  mbfposadd  37868  iunconnlem2  45175  disjrnmpt2  45432  disjinfi  45436  fsumiunss  45821  stoweidlem57  46301  fourierdlem80  46430  sge0iunmptlemre  46659  iundjiun  46704  pimiooltgt  46954  smflim  47021  smfpimcclem  47051  smfpimcc  47052  adddmmbl  47077  adddmmbl2  47078  muldmmbl  47079  muldmmbl2  47080  smfdivdmmbl2  47085