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 4958	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3261	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2897	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2889	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  ∀wral 3044  ∩ ciin 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-iin 4958

This theorem is referenced by:  dmiin  5917  scott0  9839  gruiin  10763  zarclsiin  33861  iinssiin  45123  iooiinicc  45540  iooiinioc  45554  fnlimfvre  45672  fnlimabslt  45677  meaiininclem  46484  hspdifhsp  46614  smflimlem2  46770  smflim  46775  smflimmpt  46808  smfsuplem1  46809  smfsupmpt  46813  smfsupxr  46814  smfinflem  46815  smfinfmpt  46817  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminfmpt  46830  fsupdm  46840  finfdm  46844  iinfssc  49046  iinfsubc  49047