Theorem nfiin 4981

Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2377. See nfiing 4983 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)

Hypotheses

Ref	Expression
nfiun.1	⊢ Ⅎ𝑦𝐴
nfiun.2	⊢ Ⅎ𝑦𝐵

Assertion

Ref	Expression
nfiin	⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfiin

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iin 4951	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2891	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfralw 3285	. . 3 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2905	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  ∀wral 3052  ∩ ciin 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-iin 4951

This theorem is referenced by:  iinab  5025  fnlimcnv  46054  fnlimfvre  46061  fnlimabslt  46066  iinhoiicc  47061  preimageiingt  47107  preimaleiinlt  47108  smflimlem6  47163  smflim  47164  smflim2  47193  smfsup  47201  smfsupmpt  47202  smfsupxr  47203  smfinflem  47204  smfinf  47205  smflimsup  47215  smfliminf  47218  fsupdm  47229  finfdm  47233