Theorem nfiun 4519

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)

Hypotheses

Ref	Expression
nfiun.1	⊢ Ⅎ𝑦𝐴
nfiun.2	⊢ Ⅎ𝑦𝐵

Assertion

Ref	Expression
nfiun	⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfiun

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4492	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2761	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfrex 3006	. . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2771	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2765	1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 1992  {cab 2612  Ⅎwnfc 2754  ∃wrex 2913  ∪ ciun 4490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-iun 4492

This theorem is referenced by:  iunab  4537  disjxiun  4614  disjxiunOLD  4615  ovoliunnul  23177  iundisjf  29238  iundisj2f  29239  iundisjfi  29388  iundisj2fi  29389  bnj1498  30829  trpredlem1  31420  trpredrec  31431  ss2iundf  37418  fnlimcnv  39290  fnlimfvre  39297  fnlimabslt  39302  smfaddlem1  40265  smflimlem6  40278  smflim  40279  smfmullem4  40295  smflim2  40306  smflimsup  40328