Theorem nfiin 4977

Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2374. See nfiing 4979 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 4947	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2888	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfralw 3281	. . 3 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2902	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2894	1 ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2113  {cab 2712  Ⅎwnfc 2881  ∀wral 3049  ∩ ciin 4945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-iin 4947

This theorem is referenced by:  iinab  5021  fnlimcnv  45853  fnlimfvre  45860  fnlimabslt  45865  iinhoiicc  46860  preimageiingt  46906  preimaleiinlt  46907  smflimlem6  46962  smflim  46963  smflim2  46992  smfsup  47000  smfsupmpt  47001  smfsupxr  47002  smfinflem  47003  smfinf  47004  smflimsup  47014  smfliminf  47017  fsupdm  47028  finfdm  47032