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 3308	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2986	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2977	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  {cab 2801  Ⅎwnfc 2963  ∃wrex 3141  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rex 3146  df-iun 4923

This theorem is referenced by:  ssiun2s  4974  disjxiun  5065  triun  5187  iunopeqop  5413  eliunxp  5710  opeliunxp2  5711  opeliunxp2f  7878  ixpf  8486  ixpiunwdom  9057  r1val1  9217  rankuni2b  9284  rankval4  9298  cplem2  9321  ac6num  9903  iunfo  9963  iundom2g  9964  inar1  10199  tskuni  10207  gsum2d2lem  19095  gsum2d2  19096  gsumcom2  19097  iunconn  22038  ptclsg  22225  cnextfvval  22675  ssiun2sf  30313  aciunf1lem  30409  fsumiunle  30547  esum2dlem  31353  esum2d  31354  esumiun  31355  sigapildsys  31423  bnj958  32214  bnj1000  32215  bnj981  32224  bnj1398  32308  bnj1408  32310  ralssiun  34690  iunconnlem2  41276  iunmapss  41485  iunmapsn  41487  allbutfi  41672  fsumiunss  41863  dvnprodlem1  42238  dvnprodlem2  42239  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0iunmpt  42707  iundjiun  42749  voliunsge0lem  42761  caratheodorylem2  42816  smflimmpt  43091  smflimsuplem7  43107  eliunxp2  44389