Theorem nfii1 4989

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

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

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 4954

This theorem is referenced by:  dmiin  5906  scott0  9815  gruiin  10739  zarclsiin  33854  iinssiin  45116  iooiinicc  45533  iooiinioc  45547  fnlimfvre  45665  fnlimabslt  45670  meaiininclem  46477  hspdifhsp  46607  smflimlem2  46763  smflim  46768  smflimmpt  46801  smfsuplem1  46802  smfsupmpt  46806  smfsupxr  46807  smfinflem  46808  smfinfmpt  46810  smflimsuplem7  46817  smflimsuplem8  46818  smflimsupmpt  46820  smfliminfmpt  46823  fsupdm  46833  finfdm  46837  iinfssc  49039  iinfsubc  49040