Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
|- ( ( R = S /\ A = B /\ X = Y ) -> A = B ) |
2 |
|
cnveq |
|- ( R = S -> `' R = `' S ) |
3 |
2
|
3ad2ant1 |
|- ( ( R = S /\ A = B /\ X = Y ) -> `' R = `' S ) |
4 |
|
sneq |
|- ( X = Y -> { X } = { Y } ) |
5 |
4
|
3ad2ant3 |
|- ( ( R = S /\ A = B /\ X = Y ) -> { X } = { Y } ) |
6 |
3 5
|
imaeq12d |
|- ( ( R = S /\ A = B /\ X = Y ) -> ( `' R " { X } ) = ( `' S " { Y } ) ) |
7 |
1 6
|
ineq12d |
|- ( ( R = S /\ A = B /\ X = Y ) -> ( A i^i ( `' R " { X } ) ) = ( B i^i ( `' S " { Y } ) ) ) |
8 |
|
df-pred |
|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) ) |
9 |
|
df-pred |
|- Pred ( S , B , Y ) = ( B i^i ( `' S " { Y } ) ) |
10 |
7 8 9
|
3eqtr4g |
|- ( ( R = S /\ A = B /\ X = Y ) -> Pred ( R , A , X ) = Pred ( S , B , Y ) ) |