Metamath Proof Explorer


Theorem unima

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

Ref Expression
Assertion unima FFnABACAFBC=FBFC

Proof

Step Hyp Ref Expression
1 simp1 FFnABACAFFnA
2 simpl BACABA
3 simpr BACACA
4 2 3 unssd BACABCA
5 4 3adant1 FFnABACABCA
6 1 5 fvelimabd FFnABACAyFBCxBCFx=y
7 rexun xBCFx=yxBFx=yxCFx=y
8 6 7 bitrdi FFnABACAyFBCxBFx=yxCFx=y
9 fvelimab FFnABAyFBxBFx=y
10 9 3adant3 FFnABACAyFBxBFx=y
11 fvelimab FFnACAyFCxCFx=y
12 11 3adant2 FFnABACAyFCxCFx=y
13 10 12 orbi12d FFnABACAyFByFCxBFx=yxCFx=y
14 8 13 bitr4d FFnABACAyFBCyFByFC
15 elun yFBFCyFByFC
16 14 15 bitr4di FFnABACAyFBCyFBFC
17 16 eqrdv FFnABACAFBC=FBFC