Theorem nfin 4185

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 2182, ax-11 2198, ax-12 2219. (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 3929	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1926	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1880	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2919	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 400   ∈ wcel 2149  Ⅎwnfc 2916   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-v 3465  df-in 3920

This theorem is referenced by:  inn0f  4334  csbin  4413  iunxdif3  5065  disjxun  5111  nfres  5981  nfpred  6308  cp  9876  tskwe  9935  iunconn  23553  ptclsg  23740  restmetu  24695  limciun  26021  disjunsn  32879  ordtconnlem1  34258  esum2d  34427  finminlem  36717  bj-rcleqf  37548  mbfposadd  38205  iunconnlem2  45534  disjrnmpt2  45797  disjinfi  45801  fsumiunss  46182  stoweidlem57  46662  fourierdlem80  46791  sge0iunmptlemre  47020  iundjiun  47065  pimiooltgt  47315  smflim  47382  smfpimcclem  47412  smfpimcc  47413  adddmmbl  47438  adddmmbl2  47439  muldmmbl  47440  muldmmbl2  47441  smfdivdmmbl2  47446