Theorem nfii1 4990

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 4957	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3290	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2932	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2924	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2147  {cab 2741  Ⅎwnfc 2911  ∀wral 3080  ∩ ciin 4955

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-iin 4957

This theorem is used by:  dmiin  5941  scott0b  9961  scott0OLD  9962  gruiin  10919  zarclsiin  34570  iinssiin  46347  iooiinicc  46757  iooiinioc  46771  fnlimfvre  46887  fnlimabslt  46892  meaiininclem  47699  hspdifhsp  47829  smflimlem2  47985  smflim  47990  smflimmpt  48023  smfsuplem1  48024  smfsupmpt  48028  smfsupxr  48029  smfinflem  48030  smfinfmpt  48032  smflimsuplem7  48039  smflimsuplem8  48040  smflimsupmpt  48042  smfliminfmpt  48045  fsupdm  48055  finfdm  48059  iinfssc  50374  iinfsubc  50375