Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
eluniima
Next ⟩
elunirn
Metamath Proof Explorer
Ascii
Unicode
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