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 2179, ax-11 2195, ax-12 2216. (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 3922	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2919	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2919	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2915	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  Ⅎwnfc 2912   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-in 3913

This theorem is used by:  inn0f  4326  csbin  4407  iunxdif3  5063  disjxun  5109  nfres  5982  nfpred  6311  cp  9890  tskwe  9952  iunconn  23635  ptclsg  23823  restmetu  24778  limciun  26104  disjunsn  33010  ordtconnlem1  34378  esum2d  34547  finminlem  36886  bj-rcleqf  37718  mbfposadd  38375  iunconnlem2  45701  disjrnmpt2  45964  disjinfi  45968  fsumiunss  46349  stoweidlem57  46829  fourierdlem80  46958  sge0iunmptlemre  47187  iundjiun  47232  pimiooltgt  47482  smflim  47549  smfpimcclem  47579  smfpimcc  47580  adddmmbl  47605  adddmmbl2  47606  muldmmbl  47607  muldmmbl2  47608  smfdivdmmbl2  47613