Theorem nfii1 5033

Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)

Assertion

Ref	Expression
nfii1	⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfii1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iin 5001	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3282	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2910	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2902	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2107  {cab 2710  Ⅎwnfc 2884  ∀wral 3062  ∩ ciin 4999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-iin 5001

This theorem is referenced by:  dmiin  5953  scott0  9881  gruiin  10805  zarclsiin  32851  iinssiin  43818  iooiinicc  44255  iooiinioc  44269  fnlimfvre  44390  fnlimabslt  44395  meaiininclem  45202  hspdifhsp  45332  smflimlem2  45488  smflim  45493  smflimmpt  45526  smfsuplem1  45527  smfsupmpt  45531  smfsupxr  45532  smfinflem  45533  smfinfmpt  45535  smflimsuplem7  45542  smflimsuplem8  45543  smflimsupmpt  45545  smfliminfmpt  45548  fsupdm  45558  finfdm  45562