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

Metamath Proof Explorer

Theorem nfiu1

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003) Avoid ax-11 , ax-12 . (Revised by SN, 14-May-2025)

Ref Expression
Assertion nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
2 nfre1 ⊢ Ⅎ x ∃ x ∈ A y ∈ B
3 1 2 nfxfr ⊢ Ⅎ x y ∈ ⋃ x ∈ A B
4 3 nfci ⊢ Ⅎ _ x ⋃ x ∈ A B