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 𝑥 𝑥𝐴 𝐵

Proof

Step Hyp Ref Expression
1 eliun ( 𝑦 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴 𝑦𝐵 )
2 nfre1 𝑥𝑥𝐴 𝑦𝐵
3 1 2 nfxfr 𝑥 𝑦 𝑥𝐴 𝐵
4 3 nfci 𝑥 𝑥𝐴 𝐵