This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbccsb

Description: Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007) (Revised by NM, 18-Aug-2018)

		Ref	Expression
	Assertion	sbccsb	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
2	1	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] 𝜑 )
3		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } )
4	2 3	bitr3i	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } )