cj11

Description: Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005) (Proof shortened by Eric Schmidt, 2-Jul-2009)

		Ref	Expression
	Assertion	cj11	$⊢ (A \in ℂ \land B \in ℂ) \to (\overline{A} = \overline{B} \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ \overline{A} = \overline{B} \to \overline{\overline{A}} = \overline{\overline{B}}$
2		cjcj	$⊢ A \in ℂ \to \overline{\overline{A}} = A$
3		cjcj	$⊢ B \in ℂ \to \overline{\overline{B}} = B$
4	2 3	eqeqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to (\overline{\overline{A}} = \overline{\overline{B}} \leftrightarrow A = B)$
5	1 4	imbitrid	$⊢ (A \in ℂ \land B \in ℂ) \to (\overline{A} = \overline{B} \to A = B)$
6		fveq2	$⊢ A = B \to \overline{A} = \overline{B}$
7	5 6	impbid1	$⊢ (A \in ℂ \land B \in ℂ) \to (\overline{A} = \overline{B} \leftrightarrow A = B)$

Metamath Proof Explorer