Theorem nfin 4183

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 2142, ax-11 2158, ax-12 2178. (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 3927	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2883	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2883	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1899	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1853	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2879	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Ⅎwnfc 2876   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3446  df-in 3918

This theorem is referenced by:  inn0f  4330  csbin  4401  iunxdif3  5054  disjxun  5100  nfres  5941  nfpred  6267  cp  9820  tskwe  9879  iunconn  23348  ptclsg  23535  restmetu  24491  limciun  25828  disjunsn  32573  ordtconnlem1  33907  esum2d  34076  finminlem  36299  bj-rcleqf  37006  mbfposadd  37654  iunconnlem2  44917  disjrnmpt2  45175  disjinfi  45179  fsumiunss  45566  stoweidlem57  46048  fourierdlem80  46177  sge0iunmptlemre  46406  iundjiun  46451  pimiooltgt  46701  smflim  46768  smfpimcclem  46798  smfpimcc  46799  adddmmbl  46824  adddmmbl2  46825  muldmmbl  46826  muldmmbl2  46827  smfdivdmmbl2  46832