Theorem nfii1 4986

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-iin 4953

This theorem is used by:  dmiin  5934  scott0b  9937  scott0OLD  9938  gruiin  10895  zarclsiin  34503  iinssiin  46144  iooiinicc  46554  iooiinioc  46568  fnlimfvre  46684  fnlimabslt  46689  meaiininclem  47496  hspdifhsp  47626  smflimlem2  47782  smflim  47787  smflimmpt  47820  smfsuplem1  47821  smfsupmpt  47825  smfsupxr  47826  smfinflem  47827  smfinfmpt  47829  smflimsuplem7  47836  smflimsuplem8  47837  smflimsupmpt  47839  smfliminfmpt  47842  fsupdm  47852  finfdm  47856  iinfssc  50165  iinfsubc  50166