Metamath Proof Explorer


Theorem unima

Description: Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion unima F Fn A B A C A F B C = F B F C

Proof

Step Hyp Ref Expression
1 simp1 F Fn A B A C A F Fn A
2 simpl B A C A B A
3 simpr B A C A C A
4 2 3 unssd B A C A B C A
5 4 3adant1 F Fn A B A C A B C A
6 1 5 fvelimabd F Fn A B A C A y F B C x B C F x = y
7 rexun x B C F x = y x B F x = y x C F x = y
8 6 7 bitrdi F Fn A B A C A y F B C x B F x = y x C F x = y
9 fvelimab F Fn A B A y F B x B F x = y
10 9 3adant3 F Fn A B A C A y F B x B F x = y
11 fvelimab F Fn A C A y F C x C F x = y
12 11 3adant2 F Fn A B A C A y F C x C F x = y
13 10 12 orbi12d F Fn A B A C A y F B y F C x B F x = y x C F x = y
14 8 13 bitr4d F Fn A B A C A y F B C y F B y F C
15 elun y F B F C y F B y F C
16 14 15 bitr4di F Fn A B A C A y F B C y F B F C
17 16 eqrdv F Fn A B A C A F B C = F B F C