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	|- F/_ x C
Assertion	csbiebg	|- ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )

Proof

Step	Hyp	Ref	Expression
1		csbiebg.2	|- F/_ x C
2		eqeq2	|- ( a = A -> ( x = a <-> x = A ) )
3	2	imbi1d	|- ( a = A -> ( ( x = a -> B = C ) <-> ( x = A -> B = C ) ) )
4	3	albidv	|- ( a = A -> ( A. x ( x = a -> B = C ) <-> A. x ( x = A -> B = C ) ) )
5		csbeq1	|- ( a = A -> [_ a / x ]_ B = [_ A / x ]_ B )
6	5	eqeq1d	|- ( a = A -> ( [_ a / x ]_ B = C <-> [_ A / x ]_ B = C ) )
7		vex	|- a e. _V
8	7 1	csbieb	|- ( A. x ( x = a -> B = C ) <-> [_ a / x ]_ B = C )
9	4 6 8	vtoclbg	|- ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )