theorem imaeq (_F1 _F2 _A1 _A2: set): $ _F1 == _F2 -> _A1 == _A2 -> _F1 '' _A1 == _F2 '' _A2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anl | _F1 == _F2 /\ _A1 == _A2 -> _F1 == _F2 |
|
2 | anr | _F1 == _F2 /\ _A1 == _A2 -> _A1 == _A2 |
|
3 | 1, 2 | imaeqd | _F1 == _F2 /\ _A1 == _A2 -> _F1 '' _A1 == _F2 '' _A2 |
4 | 3 | exp | _F1 == _F2 -> _A1 == _A2 -> _F1 '' _A1 == _F2 '' _A2 |