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 2175, ax-11 2191, 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 3920	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1919	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1873	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2912	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 399   ∈ wcel 2142  Ⅎwnfc 2909   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-v 3456  df-in 3911

This theorem is referenced by:  inn0f  4324  csbin  4396  iunxdif3  5052  disjxun  5098  nfres  5967  nfpred  6293  cp  9849  tskwe  9908  iunconn  23485  ptclsg  23672  restmetu  24627  limciun  25953  disjunsn  32791  ordtconnlem1  34218  esum2d  34387  finminlem  36675  bj-rcleqf  37507  mbfposadd  38163  iunconnlem2  45507  disjrnmpt2  45763  disjinfi  45767  fsumiunss  46148  stoweidlem57  46628  fourierdlem80  46757  sge0iunmptlemre  46986  iundjiun  47031  pimiooltgt  47281  smflim  47348  smfpimcclem  47378  smfpimcc  47379  adddmmbl  47404  adddmmbl2  47405  muldmmbl  47406  muldmmbl2  47407  smfdivdmmbl2  47412