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	⊢ 𝐴 ∈ V
	csbieb.2	⊢ Ⅎ 𝑥 𝐶
Assertion	csbieb	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		csbieb.1	⊢ 𝐴 ∈ V
2		csbieb.2	⊢ Ⅎ 𝑥 𝐶
3		csbiebt	⊢ ( ( 𝐴 ∈ V ∧ Ⅎ 𝑥 𝐶 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
4	1 2 3	mp2an	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )