Theorem funeq

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

	Ref	Expression
Assertion	funeq	$$⊢A=B\to \left(\mathrm{Fun}A\leftrightarrow \mathrm{Fun}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2		funss	$$⊢B\subseteq A\to \left(\mathrm{Fun}A\to \mathrm{Fun}B\right)$$
3	1 2	syl	$$⊢A=B\to \left(\mathrm{Fun}A\to \mathrm{Fun}B\right)$$
4		eqimss	$$⊢A=B\to A\subseteq B$$
5		funss	$$⊢A\subseteq B\to \left(\mathrm{Fun}B\to \mathrm{Fun}A\right)$$
6	4 5	syl	$$⊢A=B\to \left(\mathrm{Fun}B\to \mathrm{Fun}A\right)$$
7	3 6	impbid	$$⊢A=B\to \left(\mathrm{Fun}A\leftrightarrow \mathrm{Fun}B\right)$$