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