Theorem nfiu1 4955

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

Assertion

Ref	Expression
nfiu1	⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfiu1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4923	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3234	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2912	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2904	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2108  {cab 2715  Ⅎwnfc 2886  ∃wrex 3064  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rex 3069  df-iun 4923

This theorem is referenced by:  ssiun2s  4974  disjxiun  5067  triun  5200  iunopeqop  5429  eliunxp  5735  opeliunxp2  5736  opeliunxp2f  7997  ixpf  8666  ixpiunwdom  9279  r1val1  9475  rankuni2b  9542  rankval4  9556  cplem2  9579  ac6num  10166  iunfo  10226  iundom2g  10227  inar1  10462  tskuni  10470  gsum2d2lem  19489  gsum2d2  19490  gsumcom2  19491  iunconn  22487  ptclsg  22674  cnextfvval  23124  ssiun2sf  30800  djussxp2  30886  2ndresdju  30887  aciunf1lem  30901  fsumiunle  31045  esum2dlem  31960  esum2d  31961  esumiun  31962  sigapildsys  32030  bnj958  32820  bnj1000  32821  bnj981  32830  bnj1398  32914  bnj1408  32916  ralssiun  35505  iunconnlem2  42444  iunmapss  42644  iunmapsn  42646  allbutfi  42823  fsumiunss  43006  dvnprodlem1  43377  dvnprodlem2  43378  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  iundjiun  43888  voliunsge0lem  43900  caratheodorylem2  43955  smflimmpt  44230  smflimsuplem7  44246  eliunxp2  45557