Theorem nfin 4245

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 2141, 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 3992	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1898	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1851	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2896	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2108  Ⅎwnfc 2893   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-v 3490  df-in 3983

This theorem is referenced by:  inn0f  4394  csbin  4465  iunxdif3  5118  disjxun  5164  nfres  6011  nfpred  6337  cp  9960  tskwe  10019  iunconn  23457  ptclsg  23644  restmetu  24604  limciun  25949  disjunsn  32616  ordtconnlem1  33870  esum2d  34057  finminlem  36284  bj-rcleqf  36991  mbfposadd  37627  iunconnlem2  44906  disjrnmpt2  45095  disjinfi  45099  fsumiunss  45496  stoweidlem57  45978  fourierdlem80  46107  sge0iunmptlemre  46336  iundjiun  46381  pimiooltgt  46631  smflim  46698  smfpimcclem  46728  smfpimcc  46729  adddmmbl  46754  adddmmbl2  46755  muldmmbl  46756  muldmmbl2  46757  smfdivdmmbl2  46762