Theorem funALTVeq

Description: Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994)

	Ref	Expression
Assertion	funALTVeq	$$⊢A=B\to \left(FunALTVA\leftrightarrow FunALTVB\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2		funALTVss	$$⊢B\subseteq A\to \left(FunALTVA\to FunALTVB\right)$$
3	1 2	syl	$$⊢A=B\to \left(FunALTVA\to FunALTVB\right)$$
4		eqimss	$$⊢A=B\to A\subseteq B$$
5		funALTVss	$$⊢A\subseteq B\to \left(FunALTVB\to FunALTVA\right)$$
6	4 5	syl	$$⊢A=B\to \left(FunALTVB\to FunALTVA\right)$$
7	3 6	impbid	$$⊢A=B\to \left(FunALTVA\leftrightarrow FunALTVB\right)$$