Theorem csbie2t

Description: Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 ). (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 13-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		csbie2t.1	⊢ 𝐴 ∈ V
2		csbie2t.2	⊢ 𝐵 ∈ V
3		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
4		nfcvd	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → Ⅎ 𝑥 𝐷 )
5	1	a1i	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → 𝐴 ∈ V )
6		nfa2	⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
7		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝐴
8	6 7	nfan	⊢ Ⅎ 𝑦 ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 )
9		nfcvd	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → Ⅎ 𝑦 𝐷 )
10	2	a1i	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ V )
11		2sp	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) )
12	11	impl	⊢ ( ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
13	8 9 10 12	csbiedf	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )
14	3 4 5 13	csbiedf	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )