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