Theorem nfin 4177

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 2176, ax-11 2192, 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 3921	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2917	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2917	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1929	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1883	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2913	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 400   ∈ wcel 2143  Ⅎwnfc 2910   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3457  df-in 3912

This theorem is referenced by:  inn0f  4326  csbin  4407  iunxdif3  5061  disjxun  5107  nfres  5980  nfpred  6307  cp  9873  tskwe  9932  iunconn  23585  ptclsg  23772  restmetu  24727  limciun  26053  disjunsn  32939  ordtconnlem1  34314  esum2d  34483  finminlem  36829  bj-rcleqf  37661  mbfposadd  38318  iunconnlem2  45643  disjrnmpt2  45906  disjinfi  45910  fsumiunss  46291  stoweidlem57  46771  fourierdlem80  46900  sge0iunmptlemre  47129  iundjiun  47174  pimiooltgt  47424  smflim  47491  smfpimcclem  47521  smfpimcc  47522  adddmmbl  47547  adddmmbl2  47548  muldmmbl  47549  muldmmbl2  47550  smfdivdmmbl2  47555