Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
fveq2d
Next ⟩
2fveq3
Metamath Proof Explorer
Ascii
Unicode
Theorem
fveq2d
Description:
Equality deduction for function value.
(Contributed by
NM
, 29-May-1999)
Ref
Expression
Hypothesis
fveq2d.1
⊢
φ
→
A
=
B
Assertion
fveq2d
⊢
φ
→
F
⁡
A
=
F
⁡
B
Proof
Step
Hyp
Ref
Expression
1
fveq2d.1
⊢
φ
→
A
=
B
2
fveq2
⊢
A
=
B
→
F
⁡
A
=
F
⁡
B
3
1
2
syl
⊢
φ
→
F
⁡
A
=
F
⁡
B