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

Proof

Step	Hyp	Ref	Expression
1		csbieb.1	|- A e. _V
2		csbieb.2	|- F/_ x C
3		csbiebt	|- ( ( A e. _V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
4	1 2 3	mp2an	|- ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C )