Theorem csbieb

Description: Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 2-Mar-2008)

	Ref	Expression
Hypotheses	csbieb.1	$$⊢A\in \mathrm{V}$$
	csbieb.2	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	csbieb	$$⊢\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C$$

Proof

Step	Hyp	Ref	Expression
1		csbieb.1	$$⊢A\in \mathrm{V}$$
2		csbieb.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		csbiebt	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
4	1 2 3	mp2an	$$⊢\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C$$