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 A V x A B W x A B V

Proof

Step Hyp Ref Expression
1 dfiun2g x A B W x A B = y | x A y = B
2 1 adantl A V x A B W x A B = y | x A y = B
3 abrexexg A V y | x A y = B V
4 3 uniexd A V y | x A y = B V
5 4 adantr A V x A B W y | x A y = B V
6 2 5 eqeltrd A V x A B W x A B V