Theorem csbiebg

Description: Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013) (Revised by Mario Carneiro, 11-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		csbiebg.2	$$⊢\underset{\_}{Ⅎ}xC$$
2		eqeq2	$$⊢a=A\to \left(x=a\leftrightarrow x=A\right)$$
3	2	imbi1d	$$⊢a=A\to \left(\left(x=a\to B=C\right)\leftrightarrow \left(x=A\to B=C\right)\right)$$
4	3	albidv	$$⊢a=A\to \left(\forall x\left(x=a\to B=C\right)\leftrightarrow \forall x\left(x=A\to B=C\right)\right)$$
5		csbeq1	$$⊢a=A\to ⦋a/x⦌B=⦋A/x⦌B$$
6	5	eqeq1d	$$⊢a=A\to \left(⦋a/x⦌B=C\leftrightarrow ⦋A/x⦌B=C\right)$$
7		vex	$$⊢a\in \mathrm{V}$$
8	7 1	csbieb	$$⊢\forall x\left(x=a\to B=C\right)\leftrightarrow ⦋a/x⦌B=C$$
9	4 6 8	vtoclbg	$$⊢A\in V\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$