Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
imaeq2i
Next ⟩
imaeq1d
Metamath Proof Explorer
Ascii
Unicode
Theorem
imaeq2i
Description:
Equality theorem for image.
(Contributed by
NM
, 21-Dec-2008)
Ref
Expression
Hypothesis
imaeq1i.1
⊢
A
=
B
Assertion
imaeq2i
⊢
C
A
=
C
B
Proof
Step
Hyp
Ref
Expression
1
imaeq1i.1
⊢
A
=
B
2
imaeq2
⊢
A
=
B
→
C
A
=
C
B
3
1
2
ax-mp
⊢
C
A
=
C
B