Theorem nfii1 4996

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 4961	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3262	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2898	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2890	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2109  {cab 2708  Ⅎwnfc 2877  ∀wral 3045  ∩ ciin 4959

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-iin 4961

This theorem is referenced by:  dmiin  5920  scott0  9846  gruiin  10770  zarclsiin  33868  iinssiin  45130  iooiinicc  45547  iooiinioc  45561  fnlimfvre  45679  fnlimabslt  45684  meaiininclem  46491  hspdifhsp  46621  smflimlem2  46777  smflim  46782  smflimmpt  46815  smfsuplem1  46816  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinfmpt  46824  smflimsuplem7  46831  smflimsuplem8  46832  smflimsupmpt  46834  smfliminfmpt  46837  fsupdm  46847  finfdm  46851  iinfssc  49050  iinfsubc  49051