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 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2910	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  Ⅎwnfc 2907   ∩ 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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-in 3906

This theorem is used by:  inn0f  4319  csbin  4400  iunxdif3  5055  disjxun  5101  nfres  5974  nfpred  6304  cp  9893  tskwe  9955  iunconn  23653  ptclsg  23841  restmetu  24796  limciun  26121  disjunsn  33067  ordtconnlem1  34434  esum2d  34603  finminlem  36937  bj-rcleqf  37769  mbfposadd  38416  iunconnlem2  45757  disjrnmpt2  46020  disjinfi  46024  fsumiunss  46405  stoweidlem57  46885  fourierdlem80  47014  sge0iunmptlemre  47243  iundjiun  47288  pimiooltgt  47538  smflim  47605  smfpimcclem  47635  smfpimcc  47636  adddmmbl  47661  adddmmbl2  47662  muldmmbl  47663  muldmmbl2  47664  smfdivdmmbl2  47669