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  5937  scott0b  9877  scott0OLD  9878  gruiin  10820  zarclsiin  34382  iinssiin  45962  iooiinicc  46373  iooiinioc  46387  fnlimfvre  46503  fnlimabslt  46508  meaiininclem  47315  hspdifhsp  47445  smflimlem2  47601  smflim  47606  smflimmpt  47639  smfsuplem1  47640  smfsupmpt  47644  smfsupxr  47645  smfinflem  47646  smfinfmpt  47648  smflimsuplem7  47655  smflimsuplem8  47656  smflimsupmpt  47658  smfliminfmpt  47661  fsupdm  47671  finfdm  47675  iinfssc  49984  iinfsubc  49985