Theorem csb2

Description: Alternate expression for the proper substitution into a class, without referencing substitution into a wff. Note that x can be free in B but cannot occur in A . (Contributed by NM, 2-Dec-2013)

	Ref	Expression
Assertion	csb2	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
2		sbc5	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3	2	abbii	⊢ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
4	1 3	eqtri	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) }