Theorem nfiu1 4964

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 4932	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3237	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2915	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2907	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2110  {cab 2717  Ⅎwnfc 2889  ∃wrex 3067  ∪ ciun 4930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-rex 3072  df-iun 4932

This theorem is referenced by:  ssiun2s  4983  disjxiun  5076  triun  5209  iunopeqop  5438  eliunxp  5744  opeliunxp2  5745  opeliunxp2f  8011  ixpf  8683  ixpiunwdom  9319  r1val1  9537  rankuni2b  9604  rankval4  9618  cplem2  9641  ac6num  10228  iunfo  10288  iundom2g  10289  inar1  10524  tskuni  10532  gsum2d2lem  19564  gsum2d2  19565  gsumcom2  19566  iunconn  22569  ptclsg  22756  cnextfvval  23206  ssiun2sf  30887  djussxp2  30973  2ndresdju  30974  aciunf1lem  30987  fsumiunle  31131  esum2dlem  32048  esum2d  32049  esumiun  32050  sigapildsys  32118  bnj958  32908  bnj1000  32909  bnj981  32918  bnj1398  33002  bnj1408  33004  ralssiun  35566  iunconnlem2  42517  iunmapss  42717  iunmapsn  42719  allbutfi  42896  fsumiunss  43079  dvnprodlem1  43450  dvnprodlem2  43451  sge0iunmptlemfi  43914  sge0iunmptlemre  43916  sge0iunmpt  43919  iundjiun  43961  voliunsge0lem  43973  caratheodorylem2  44028  smflimmpt  44303  smflimsuplem7  44319  eliunxp2  45630