Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Functions
funALTVeqd
Next ⟩
Disjoints vs. converse functions
Metamath Proof Explorer
Ascii
Unicode
Theorem
funALTVeqd
Description:
Equality deduction for the function predicate.
(Contributed by
NM
, 23-Feb-2013)
Ref
Expression
Hypothesis
funALTVeqd.1
⊢
φ
→
A
=
B
Assertion
funALTVeqd
⊢
φ
→
FunALTV
A
↔
FunALTV
B
Proof
Step
Hyp
Ref
Expression
1
funALTVeqd.1
⊢
φ
→
A
=
B
2
funALTVeq
⊢
A
=
B
→
FunALTV
A
↔
FunALTV
B
3
1
2
syl
⊢
φ
→
FunALTV
A
↔
FunALTV
B