Theorem nfii1 5052

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 5018	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3290	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2914	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	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-or 847  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:  dmiin  5978  scott0  9955  gruiin  10879  zarclsiin  33817  iinssiin  45031  iooiinicc  45460  iooiinioc  45474  fnlimfvre  45595  fnlimabslt  45600  meaiininclem  46407  hspdifhsp  46537  smflimlem2  46693  smflim  46698  smflimmpt  46731  smfsuplem1  46732  smfsupmpt  46736  smfsupxr  46737  smfinflem  46738  smfinfmpt  46740  smflimsuplem7  46747  smflimsuplem8  46748  smflimsupmpt  46750  smfliminfmpt  46753  fsupdm  46763  finfdm  46767