Theorem nfiin 5047

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

Syntax hints:   ∈ wcel 2108  {cab 2717  Ⅎwnfc 2893  ∀wral 3067  ∩ ciin 5016

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-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-iin 5018

This theorem is referenced by:  iinab  5091  fnlimcnv  45588  fnlimfvre  45595  fnlimabslt  45600  iinhoiicc  46595  preimageiingt  46641  preimaleiinlt  46642  smflimlem6  46697  smflim  46698  smflim2  46727  smfsup  46735  smfsupmpt  46736  smfsupxr  46737  smfinflem  46738  smfinf  46739  smfinfmpt  46740  smflimsup  46749  smfliminf  46752  fsupdm  46763  finfdm  46767