Theorem dmeq

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

	Ref	Expression
Assertion	dmeq	|- ( A = B -> dom A = dom B )

Proof

Step	Hyp	Ref	Expression
1		dmss	|- ( A C_ B -> dom A C_ dom B )
2		dmss	|- ( B C_ A -> dom B C_ dom A )
3	1 2	anim12i	|- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss	|- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3 4 5	3imtr4i	|- ( A = B -> dom A = dom B )