Theorem nfin 4153

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 2152, ax-11 2168, ax-12 2189. (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 3899	. . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfin.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2893	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfin.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2893	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1860	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵)
8	7	nfci 2889	1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵)

Syntax hints:   ∧ wa 396   ∈ wcel 2119  Ⅎwnfc 2886   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-v 3433  df-in 3890

This theorem is referenced by:  inn0f  4299  csbin  4370  iunxdif3  5024  disjxun  5070  nfres  5933  nfpred  6257  cp  9806  tskwe  9865  iunconn  23411  ptclsg  23598  restmetu  24553  limciun  25879  disjunsn  32683  ordtconnlem1  34108  esum2d  34277  finminlem  36546  bj-rcleqf  37378  mbfposadd  38034  iunconnlem2  45378  disjrnmpt2  45635  disjinfi  45639  fsumiunss  46020  stoweidlem57  46500  fourierdlem80  46629  sge0iunmptlemre  46858  iundjiun  46903  pimiooltgt  47153  smflim  47220  smfpimcclem  47250  smfpimcc  47251  adddmmbl  47276  adddmmbl2  47277  muldmmbl  47278  muldmmbl2  47279  smfdivdmmbl2  47284