Theorem csbie2

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007)

	Ref	Expression
Hypotheses	csbie2t.1	⊢ 𝐴 ∈ V
	csbie2t.2	⊢ 𝐵 ∈ V
	csbie2.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
Assertion	csbie2	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷

Proof

Step	Hyp	Ref	Expression
1		csbie2t.1	⊢ 𝐴 ∈ V
2		csbie2t.2	⊢ 𝐵 ∈ V
3		csbie2.3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
4	3	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
5	1 2	csbie2t	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )
6	4 5	ax-mp	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷