Theorem nfii1 4916

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 4884	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3183	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2961	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2953	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  ∀wral 3106  ∩ ciin 4882

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-iin 4884

This theorem is referenced by:  dmiin  5789  scott0  9299  gruiin  10221  zarclsiin  31224  iinssiin  41764  iooiinicc  42179  iooiinioc  42193  fnlimfvre  42316  fnlimabslt  42321  meaiininclem  43125  hspdifhsp  43255  smflimlem2  43405  smflim  43410  smflimmpt  43441  smfsuplem1  43442  smfsupmpt  43446  smfsupxr  43447  smfinflem  43448  smfinfmpt  43450  smflimsuplem7  43457  smflimsuplem8  43458  smflimsupmpt  43460  smfliminfmpt  43463