Theorem nfii1 4991

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cab 2740  Ⅎwnfc 2909  ∀wral 3078  ∩ 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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-iin 4957

This theorem is used by:  dmiin  5941  scott0b  9879  scott0OLD  9880  gruiin  10820  zarclsiin  34366  iinssiin  45946  iooiinicc  46357  iooiinioc  46371  fnlimfvre  46487  fnlimabslt  46492  meaiininclem  47299  hspdifhsp  47429  smflimlem2  47585  smflim  47590  smflimmpt  47623  smfsuplem1  47624  smfsupmpt  47628  smfsupxr  47629  smfinflem  47630  smfinfmpt  47632  smflimsuplem7  47639  smflimsuplem8  47640  smflimsupmpt  47642  smfliminfmpt  47645  fsupdm  47655  finfdm  47659  iinfssc  49968  iinfsubc  49969