Theorem dmeq

Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994)

	Ref	Expression
Assertion	dmeq	$$⊢A=B\to \mathrm{dom}A=\mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		dmss	$$⊢A\subseteq B\to \mathrm{dom}A\subseteq \mathrm{dom}B$$
2		dmss	$$⊢B\subseteq A\to \mathrm{dom}B\subseteq \mathrm{dom}A$$
3	1 2	anim12i	$$⊢\left(A\subseteq B\wedge B\subseteq A\right)\to \left(\mathrm{dom}A\subseteq \mathrm{dom}B\wedge \mathrm{dom}B\subseteq \mathrm{dom}A\right)$$
4		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
5		eqss	$$⊢\mathrm{dom}A=\mathrm{dom}B\leftrightarrow \left(\mathrm{dom}A\subseteq \mathrm{dom}B\wedge \mathrm{dom}B\subseteq \mathrm{dom}A\right)$$
6	3 4 5	3imtr4i	$$⊢A=B\to \mathrm{dom}A=\mathrm{dom}B$$