Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
fveq12i
Next ⟩
fveq12d
Metamath Proof Explorer
Ascii
Unicode
Theorem
fveq12i
Description:
Equality deduction for function value.
(Contributed by
FL
, 27-Jun-2014)
Ref
Expression
Hypotheses
fveq12i.1
⊢
F
=
G
fveq12i.2
⊢
A
=
B
Assertion
fveq12i
⊢
F
⁡
A
=
G
⁡
B
Proof
Step
Hyp
Ref
Expression
1
fveq12i.1
⊢
F
=
G
2
fveq12i.2
⊢
A
=
B
3
1
fveq1i
⊢
F
⁡
A
=
G
⁡
A
4
2
fveq2i
⊢
G
⁡
A
=
G
⁡
B
5
3
4
eqtri
⊢
F
⁡
A
=
G
⁡
B