Theorem nfii1 4993

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 4959	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3289	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2931	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2923	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2143  {cab 2741  Ⅎwnfc 2910  ∀wral 3079  ∩ ciin 4957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-iin 4959

This theorem is used by:  dmiin  5943  scott0b  9862  scott0OLD  9863  gruiin  10799  zarclsiin  34270  iinssiin  45875  iooiinicc  46286  iooiinioc  46300  fnlimfvre  46416  fnlimabslt  46421  meaiininclem  47228  hspdifhsp  47358  smflimlem2  47514  smflim  47519  smflimmpt  47552  smfsuplem1  47553  smfsupmpt  47557  smfsupxr  47558  smfinflem  47559  smfinfmpt  47561  smflimsuplem7  47568  smflimsuplem8  47569  smflimsupmpt  47571  smfliminfmpt  47574  fsupdm  47584  finfdm  47588  iinfssc  49863  iinfsubc  49864