Metamath Proof Explorer


Theorem iunexg

Description: The existence of an indexed union. x is normally a free-variable parameter in B . (Contributed by NM, 23-Mar-2006)

Ref Expression
Assertion iunexg AVxABWxABV

Proof

Step Hyp Ref Expression
1 dfiun2g xABWxAB=y|xAy=B
2 1 adantl AVxABWxAB=y|xAy=B
3 abrexexg AVy|xAy=BV
4 3 uniexd AVy|xAy=BV
5 4 adantr AVxABWy|xAy=BV
6 2 5 eqeltrd AVxABWxABV