This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfiun

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014) Add disjoint variable condition to avoid ax-13 . See nfiung for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024)

Ref Expression
Hypotheses nfiun.1 ⊢ Ⅎ _ y A
nfiun.2 ⊢ Ⅎ _ y B
Assertion nfiun ⊢ Ⅎ _ y ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 nfiun.1 ⊢ Ⅎ _ y A
2 nfiun.2 ⊢ Ⅎ _ y B
3 df-iun ⊢ ⋃ x ∈ A B = z | ∃ x ∈ A z ∈ B
4 2 nfcri ⊢ Ⅎ y z ∈ B
5 1 4 nfrexw ⊢ Ⅎ y ∃ x ∈ A z ∈ B
6 5 nfab ⊢ Ⅎ _ y z | ∃ x ∈ A z ∈ B
7 3 6 nfcxfr ⊢ Ⅎ _ y ⋃ x ∈ A B