Theorem nfin 4170

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 2178, ax-11 2194, ax-12 2213. (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 3915	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2911	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2908   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-in 3906

This theorem is used by:  inn0f  4319  csbin  4400  iunxdif3  5055  disjxun  5101  nfres  5972  nfpred  6308  cp  9947  tskwe  10024  iunconn  23739  ptclsg  23927  restmetu  24882  limciun  26207  disjunsn  33181  ordtconnlem1  34549  esum2d  34718  finminlem  37086  bj-rcleqf  37918  mbfposadd  38565  iunconnlem2  45902  disjrnmpt2  46172  disjinfi  46176  fsumiunss  46556  stoweidlem57  47036  fourierdlem80  47165  sge0iunmptlemre  47394  iundjiun  47439  pimiooltgt  47689  smflim  47756  smfpimcclem  47786  smfpimcc  47787  adddmmbl  47812  adddmmbl2  47813  muldmmbl  47814  muldmmbl2  47815  smfdivdmmbl2  47820