Theorem nfii1 4959

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 4925	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3263	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2907	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2899	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2119  {cab 2717  Ⅎwnfc 2886  ∀wral 3053  ∩ ciin 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-iin 4925

This theorem is referenced by:  dmiin  5896  scott0  9802  gruiin  10725  zarclsiin  34064  iinssiin  45584  iooiinicc  45995  iooiinioc  46009  fnlimfvre  46125  fnlimabslt  46130  meaiininclem  46937  hspdifhsp  47067  smflimlem2  47223  smflim  47228  smflimmpt  47261  smfsuplem1  47262  smfsupmpt  47266  smfsupxr  47267  smfinflem  47268  smfinfmpt  47270  smflimsuplem7  47277  smflimsuplem8  47278  smflimsupmpt  47280  smfliminfmpt  47283  fsupdm  47293  finfdm  47297  iinfssc  49555  iinfsubc  49556