Theorem nfii1 4987

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 4954	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3286	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2928	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2920	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2145  {cab 2738  Ⅎwnfc 2907  ∀wral 3076  ∩ ciin 4952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-iin 4954

This theorem is used by:  dmiin  5939  scott0b  9901  scott0OLD  9902  gruiin  10844  zarclsiin  34414  iinssiin  46026  iooiinicc  46437  iooiinioc  46451  fnlimfvre  46567  fnlimabslt  46572  meaiininclem  47379  hspdifhsp  47509  smflimlem2  47665  smflim  47670  smflimmpt  47703  smfsuplem1  47704  smfsupmpt  47708  smfsupxr  47709  smfinflem  47710  smfinfmpt  47712  smflimsuplem7  47719  smflimsuplem8  47720  smflimsupmpt  47722  smfliminfmpt  47725  fsupdm  47735  finfdm  47739  iinfssc  50048  iinfsubc  50049