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

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

Proof of Theorem domcmpd
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 fveq2 5541 . . . . . . . 8
98eqeq2d 2307 . . . . . . 7
10 oveq2 5882 . . . . . . . . 9
1110fveq2d 5545 . . . . . . . 8
12 fveq2 5541 . . . . . . . 8
1311, 12eqeq12d 2310 . . . . . . 7
149, 13imbi12d 311 . . . . . 6
15 fveq2 5541 . . . . . . . 8
1615eqeq1d 2304 . . . . . . 7
17 oveq1 5881 . . . . . . . . 9
1817fveq2d 5545 . . . . . . . 8
1918eqeq1d 2304 . . . . . . 7
2016, 19imbi12d 311 . . . . . 6
2114, 20rspc2v 2903 . . . . 5
2221com12 27 . . . 4