Metamath Proof Explorer


Theorem eluniima

Description: Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion eluniima Fun F B F A x A B F x

Proof

Step Hyp Ref Expression
1 funiunfv Fun F x A F x = F A
2 1 eleq2d Fun F B x A F x B F A
3 eliun B x A F x x A B F x
4 2 3 bitr3di Fun F B F A x A B F x