Theorem nfii1 4971

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 4936	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3261	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2904	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2896	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  {cab 2714  Ⅎwnfc 2883  ∀wral 3051  ∩ ciin 4934

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-iin 4936

This theorem is referenced by:  dmiin  5908  scott0  9810  gruiin  10733  zarclsiin  34015  iinssiin  45559  iooiinicc  45972  iooiinioc  45986  fnlimfvre  46102  fnlimabslt  46107  meaiininclem  46914  hspdifhsp  47044  smflimlem2  47200  smflim  47205  smflimmpt  47238  smfsuplem1  47239  smfsupmpt  47243  smfsupxr  47244  smfinflem  47245  smfinfmpt  47247  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  fsupdm  47270  finfdm  47274  iinfssc  49532  iinfsubc  49533