Description: Lemma for showing the equality of values for functions like slot extractors E at a proper class. Extracted from several former proofs of lemmas like resvlem . (Contributed by AV, 31-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | oveqprc.e | |- ( E ` (/) ) = (/) |
|
| oveqprc.z | |- Z = ( X O Y ) |
||
| oveqprc.r | |- Rel dom O |
||
| Assertion | oveqprc | |- ( -. X e. _V -> ( E ` X ) = ( E ` Z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveqprc.e | |- ( E ` (/) ) = (/) |
|
| 2 | oveqprc.z | |- Z = ( X O Y ) |
|
| 3 | oveqprc.r | |- Rel dom O |
|
| 4 | 1 | eqcomi | |- (/) = ( E ` (/) ) |
| 5 | fvprc | |- ( -. X e. _V -> ( E ` X ) = (/) ) |
|
| 6 | 3 | ovprc1 | |- ( -. X e. _V -> ( X O Y ) = (/) ) |
| 7 | 2 6 | eqtrid | |- ( -. X e. _V -> Z = (/) ) |
| 8 | 7 | fveq2d | |- ( -. X e. _V -> ( E ` Z ) = ( E ` (/) ) ) |
| 9 | 4 5 8 | 3eqtr4a | |- ( -. X e. _V -> ( E ` X ) = ( E ` Z ) ) |