Theorem nfiu1 4486

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 4457	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 2988	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2755	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2749	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 1977  {cab 2596  Ⅎwnfc 2738  ∃wrex 2897  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-iun 4457

This theorem is referenced by:  ssiun2s  4500  disjxiun  4579  disjxiunOLD  4580  triun  4694  iunopeqop  4906  eliunxp  5181  opeliunxp2  5182  opeliunxp2f  7223  ixpf  7816  ixpiunwdom  8379  r1val1  8532  rankuni2b  8599  rankval4  8613  cplem2  8636  ac6num  9184  iunfo  9240  iundom2g  9241  inar1  9476  tskuni  9484  gsum2d2lem  18195  gsum2d2  18196  gsumcom2  18197  iuncon  21041  ptclsg  21228  cnextfvval  21679  ssiun2sf  28760  aciunf1lem  28844  esum2dlem  29481  esum2d  29482  esumiun  29483  sigapildsys  29552  bnj958  30264  bnj1000  30265  bnj981  30274  bnj1398  30356  bnj1408  30358  iunconlem2  38193  iunmapss  38402  iunmapsn  38404  allbutfi  38557  fsumiunss  38642  dvnprodlem1  38836  dvnprodlem2  38837  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  iundjiun  39353  voliunsge0lem  39365  caratheodorylem2  39417  eliunxp2  41905