Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  codcmpd Unicode version

Theorem codcmpd 25747
 Description: When is defined its codomain is the codomain of . (Contributed by FL, 29-Oct-2007.)
Hypotheses
Ref Expression
ded.1
ded.2
ded.3
ded.4
Assertion
Ref Expression
codcmpd

Proof of Theorem codcmpd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ded.2 . . . 4
2 ded.3 . . . 4
3 eqid 2283 . . . 4
4 ded.4 . . . 4
5 ded.1 . . . 4
6 eqid 2283 . . . 4
71, 2, 3, 4, 5, 6dedi 25737 . . 3
8 fveq2 5525 . . . . . . . 8
98eqeq2d 2294 . . . . . . 7
10 oveq2 5866 . . . . . . . . 9
1110fveq2d 5529 . . . . . . . 8
1211eqeq1d 2291 . . . . . . 7
139, 12imbi12d 311 . . . . . 6
14 fveq2 5525 . . . . . . . 8
1514eqeq1d 2291 . . . . . . 7
16 oveq1 5865 . . . . . . . . 9
1716fveq2d 5529 . . . . . . . 8
18 fveq2 5525 . . . . . . . 8
1917, 18eqeq12d 2297 . . . . . . 7
2015, 19imbi12d 311 . . . . . 6
2113, 20rspc2v 2890 . . . . 5
2221com12 27 . . . 4