Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Functions
funALTVeq
Next ⟩
funALTVeqi
Metamath Proof Explorer
Ascii
Unicode
Theorem
funALTVeq
Description:
Equality theorem for function predicate.
(Contributed by
NM
, 16-Aug-1994)
Ref
Expression
Assertion
funALTVeq
⊢
A
=
B
→
FunALTV
A
↔
FunALTV
B
Proof
Step
Hyp
Ref
Expression
1
eqimss2
⊢
A
=
B
→
B
⊆
A
2
funALTVss
⊢
B
⊆
A
→
FunALTV
A
→
FunALTV
B
3
1
2
syl
⊢
A
=
B
→
FunALTV
A
→
FunALTV
B
4
eqimss
⊢
A
=
B
→
A
⊆
B
5
funALTVss
⊢
A
⊆
B
→
FunALTV
B
→
FunALTV
A
6
4
5
syl
⊢
A
=
B
→
FunALTV
B
→
FunALTV
A
7
3
6
impbid
⊢
A
=
B
→
FunALTV
A
↔
FunALTV
B