Theorem nfii1 4972

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 4937	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3262	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2905	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2897	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  ∀wral 3052  ∩ ciin 4935

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-iin 4937

This theorem is referenced by:  dmiin  5904  scott0  9805  gruiin  10728  zarclsiin  34035  iinssiin  45581  iooiinicc  45994  iooiinioc  46008  fnlimfvre  46124  fnlimabslt  46129  meaiininclem  46936  hspdifhsp  47066  smflimlem2  47222  smflim  47227  smflimmpt  47260  smfsuplem1  47261  smfsupmpt  47265  smfsupxr  47266  smfinflem  47267  smfinfmpt  47269  smflimsuplem7  47276  smflimsuplem8  47277  smflimsupmpt  47279  smfliminfmpt  47282  fsupdm  47292  finfdm  47296  iinfssc  49548  iinfsubc  49549