Theorem nfiu1 4945

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 4913	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3306	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2984	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2975	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2110  {cab 2799  Ⅎwnfc 2961  ∃wrex 3139  ∪ ciun 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-iun 4913

This theorem is referenced by:  ssiun2s  4964  disjxiun  5055  triun  5177  iunopeqop  5403  eliunxp  5702  opeliunxp2  5703  opeliunxp2f  7870  ixpf  8478  ixpiunwdom  9049  r1val1  9209  rankuni2b  9276  rankval4  9290  cplem2  9313  ac6num  9895  iunfo  9955  iundom2g  9956  inar1  10191  tskuni  10199  gsum2d2lem  19087  gsum2d2  19088  gsumcom2  19089  iunconn  22030  ptclsg  22217  cnextfvval  22667  ssiun2sf  30305  aciunf1lem  30401  fsumiunle  30540  esum2dlem  31346  esum2d  31347  esumiun  31348  sigapildsys  31416  bnj958  32207  bnj1000  32208  bnj981  32217  bnj1398  32301  bnj1408  32303  ralssiun  34682  iunconnlem2  41262  iunmapss  41471  iunmapsn  41473  allbutfi  41658  fsumiunss  41849  dvnprodlem1  42224  dvnprodlem2  42225  sge0iunmptlemfi  42689  sge0iunmptlemre  42691  sge0iunmpt  42694  iundjiun  42736  voliunsge0lem  42748  caratheodorylem2  42803  smflimmpt  43078  smflimsuplem7  43094  eliunxp2  44376