Theorem sbc5

Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by SN, 2-Sep-2024)

	Ref	Expression
Assertion	sbc5	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
2		clelab	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
3	1 2	bitri	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )