Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
2fveq3
Next ⟩
fveq12i
Metamath Proof Explorer
Ascii
Unicode
Theorem
2fveq3
Description:
Equality theorem for nested function values.
(Contributed by
AV
, 14-Aug-2022)
Ref
Expression
Assertion
2fveq3
⊢
A
=
B
→
F
⁡
G
⁡
A
=
F
⁡
G
⁡
B
Proof
Step
Hyp
Ref
Expression
1
fveq2
⊢
A
=
B
→
G
⁡
A
=
G
⁡
B
2
1
fveq2d
⊢
A
=
B
→
F
⁡
G
⁡
A
=
F
⁡
G
⁡
B