Theorem nfii1 4988

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

Syntax hints:   ∈ wcel 2144  {cab 2742  Ⅎwnfc 2911  ∀wral 3078  ∩ ciin 4952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ral 3079  df-iin 4954

This theorem is referenced by:  dmiin  5931  scott0  9846  gruiin  10770  zarclsiin  34170  iinssiin  45712  iooiinicc  46123  iooiinioc  46137  fnlimfvre  46253  fnlimabslt  46258  meaiininclem  47065  hspdifhsp  47195  smflimlem2  47351  smflim  47356  smflimmpt  47389  smfsuplem1  47390  smfsupmpt  47394  smfsupxr  47395  smfinflem  47396  smfinfmpt  47398  smflimsuplem7  47405  smflimsuplem8  47406  smflimsupmpt  47408  smfliminfmpt  47411  fsupdm  47421  finfdm  47425  iinfssc  49683  iinfsubc  49684