Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Relations and Functions
Functions - misc additions
unipreima
Next ⟩
sspreima
Metamath Proof Explorer
Ascii
Unicode
Theorem
unipreima
Description:
Preimage of a class union.
(Contributed by
Thierry Arnoux
, 7-Feb-2017)
Ref
Expression
Assertion
unipreima
⊢
Fun
⁡
F
→
F
-1
⋃
A
=
⋃
x
∈
A
F
-1
x
Proof
Step
Hyp
Ref
Expression
1
funfn
⊢
Fun
⁡
F
↔
F
Fn
dom
⁡
F
2
r19.42v
⊢
∃
x
∈
A
y
∈
dom
⁡
F
∧
F
⁡
y
∈
x
↔
y
∈
dom
⁡
F
∧
∃
x
∈
A
F
⁡
y
∈
x
3
2
bicomi
⊢
y
∈
dom
⁡
F
∧
∃
x
∈
A
F
⁡
y
∈
x
↔
∃
x
∈
A
y
∈
dom
⁡
F
∧
F
⁡
y
∈
x
4
3
a1i
⊢
F
Fn
dom
⁡
F
→
y
∈
dom
⁡
F
∧
∃
x
∈
A
F
⁡
y
∈
x
↔
∃
x
∈
A
y
∈
dom
⁡
F
∧
F
⁡
y
∈
x
5
eluni2
⊢
F
⁡
y
∈
⋃
A
↔
∃
x
∈
A
F
⁡
y
∈
x
6
5
anbi2i
⊢
y
∈
dom
⁡
F
∧
F
⁡
y
∈
⋃
A
↔
y
∈
dom
⁡
F
∧
∃
x
∈
A
F
⁡
y
∈
x
7
6
a1i
⊢
F
Fn
dom
⁡
F
→
y
∈
dom
⁡
F
∧
F
⁡
y
∈
⋃
A
↔
y
∈
dom
⁡
F
∧
∃
x
∈
A
F
⁡
y
∈
x
8
elpreima
⊢
F
Fn
dom
⁡
F
→
y
∈
F
-1
x
↔
y
∈
dom
⁡
F
∧
F
⁡
y
∈
x
9
8
rexbidv
⊢
F
Fn
dom
⁡
F
→
∃
x
∈
A
y
∈
F
-1
x
↔
∃
x
∈
A
y
∈
dom
⁡
F
∧
F
⁡
y
∈
x
10
4
7
9
3bitr4d
⊢
F
Fn
dom
⁡
F
→
y
∈
dom
⁡
F
∧
F
⁡
y
∈
⋃
A
↔
∃
x
∈
A
y
∈
F
-1
x
11
elpreima
⊢
F
Fn
dom
⁡
F
→
y
∈
F
-1
⋃
A
↔
y
∈
dom
⁡
F
∧
F
⁡
y
∈
⋃
A
12
eliun
⊢
y
∈
⋃
x
∈
A
F
-1
x
↔
∃
x
∈
A
y
∈
F
-1
x
13
12
a1i
⊢
F
Fn
dom
⁡
F
→
y
∈
⋃
x
∈
A
F
-1
x
↔
∃
x
∈
A
y
∈
F
-1
x
14
10
11
13
3bitr4d
⊢
F
Fn
dom
⁡
F
→
y
∈
F
-1
⋃
A
↔
y
∈
⋃
x
∈
A
F
-1
x
15
14
eqrdv
⊢
F
Fn
dom
⁡
F
→
F
-1
⋃
A
=
⋃
x
∈
A
F
-1
x
16
1
15
sylbi
⊢
Fun
⁡
F
→
F
-1
⋃
A
=
⋃
x
∈
A
F
-1
x