Theorem nfii1 4982

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 4947	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3258	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2902	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	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-or 848  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:  dmiin  5900  scott0  9796  gruiin  10719  zarclsiin  33977  iinssiin  45315  iooiinicc  45730  iooiinioc  45744  fnlimfvre  45860  fnlimabslt  45865  meaiininclem  46672  hspdifhsp  46802  smflimlem2  46958  smflim  46963  smflimmpt  46996  smfsuplem1  46997  smfsupmpt  47001  smfsupxr  47002  smfinflem  47003  smfinfmpt  47005  smflimsuplem7  47012  smflimsuplem8  47013  smflimsupmpt  47015  smfliminfmpt  47018  fsupdm  47028  finfdm  47032  iinfssc  49244  iinfsubc  49245