Theorem nfii1 5005

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 4970	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfra1 3266	. . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2904	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2896	1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2108  {cab 2713  Ⅎwnfc 2883  ∀wral 3051  ∩ ciin 4968

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-iin 4970

This theorem is referenced by:  dmiin  5933  scott0  9900  gruiin  10824  zarclsiin  33902  iinssiin  45153  iooiinicc  45571  iooiinioc  45585  fnlimfvre  45703  fnlimabslt  45708  meaiininclem  46515  hspdifhsp  46645  smflimlem2  46801  smflim  46806  smflimmpt  46839  smfsuplem1  46840  smfsupmpt  46844  smfsupxr  46845  smfinflem  46846  smfinfmpt  46848  smflimsuplem7  46855  smflimsuplem8  46856  smflimsupmpt  46858  smfliminfmpt  46861  fsupdm  46871  finfdm  46875  iinfssc  49024  iinfsubc  49025