Theorem nfii1 4551

Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.)

Assertion

Ref	Expression
nfii1	|- F/_ x |^|_ x e. A B

Proof of Theorem nfii1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iin 4523	. 2 |- |^|_ x e. A B = { y | A. x e. A y e. B }
2		nfra1 2941	. . 3 |- F/ x A. x e. A y e. B
3	2	nfab 2769	. 2 |- F/_ x { y | A. x e. A y e. B }
4	1, 3	nfcxfr 2762	1 |- F/_ x |^|_ x e. A B

Syntax hints:   e. wcel 1990   {cab 2608   F/_wnfc 2751   A.wral 2912   |^|_ciin 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-iin 4523

This theorem is referenced by:  dmiin  5369  scott0  8749  gruiin  9632  iinssiin  39312  iooiinicc  39769  iooiinioc  39783  fnlimfvre  39906  fnlimabslt  39911  meaiininclem  40700  hspdifhsp  40830  smflimlem2  40980  smflim  40985  smflimmpt  41016  smfsuplem1  41017  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinfmpt  41025  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminfmpt  41038