Theorem nfin 4187

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 3930	. . 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 3913

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 3449  df-in 3921

This theorem is referenced by:  inn0f  4334  csbin  4405  iunxdif3  5059  disjxun  5105  nfres  5952  nfpred  6279  cp  9844  tskwe  9903  iunconn  23315  ptclsg  23502  restmetu  24458  limciun  25795  disjunsn  32523  ordtconnlem1  33914  esum2d  34083  finminlem  36306  bj-rcleqf  37013  mbfposadd  37661  iunconnlem2  44924  disjrnmpt2  45182  disjinfi  45186  fsumiunss  45573  stoweidlem57  46055  fourierdlem80  46184  sge0iunmptlemre  46413  iundjiun  46458  pimiooltgt  46708  smflim  46775  smfpimcclem  46805  smfpimcc  46806  adddmmbl  46831  adddmmbl2  46832  muldmmbl  46833  muldmmbl2  46834  smfdivdmmbl2  46839