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

Theorem cmppfd 25848
 Description: is only defined when the domain of is the codomain of . (Contributed by FL, 29-Oct-2007.)
Hypotheses
Ref Expression
ded.1
ded.2
ded.3
ded.4
Assertion
Ref Expression
cmppfd

Proof of Theorem cmppfd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ded.2 . . . 4
2 ded.3 . . . 4
3 eqid 2296 . . . 4
4 ded.4 . . . 4
5 ded.1 . . . 4
6 eqid 2296 . . . 4
71, 2, 3, 4, 5, 6dedi 25840 . . 3
8 opeq2 3813 . . . . . . . . 9
98eleq1d 2362 . . . . . . . 8
10 fveq2 5541 . . . . . . . . 9
1110eqeq2d 2307 . . . . . . . 8
129, 11bibi12d 312 . . . . . . 7
13 opeq1 3812 . . . . . . . . 9
1413eleq1d 2362 . . . . . . . 8
15 fveq2 5541 . . . . . . . . 9
1615eqeq1d 2304 . . . . . . . 8
1714, 16bibi12d 312 . . . . . . 7
1812, 17rspc2v 2903 . . . . . 6
1918com12 27 . . . . 5
20193ad2ant3 978 . . . 4