Theorem nfin 4120

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 2177, ax-11 2193, ax-12 2212. (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 4092	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1931	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1885	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2910	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2144  Ⅎwnfc 2907   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-in 4090

This theorem is used by:  inn0f  4318  csbin  4399  iunxdif3  5054  disjxun  5100  nfres  5973  nfpred  6312  cp  9961  tskwe  10038  iunconn  23755  ptclsg  23943  restmetu  24898  limciun  26223  disjunsn  33239  ordtconnlem1  34606  esum2d  34775  finminlem  37230  bj-rcleqf  38062  mbfposadd  38722  iunconnlem2  46053  disjrnmpt2  46339  disjinfi  46343  fsumiunss  46723  stoweidlem57  47203  fourierdlem80  47332  sge0iunmptlemre  47561  iundjiun  47606  pimiooltgt  47856  smflim  47923  smfpimcclem  47953  smfpimcc  47954  adddmmbl  47979  adddmmbl2  47980  muldmmbl  47981  muldmmbl2  47982  smfdivdmmbl2  47987