Theorem sbccsb2

Description: Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005) (Revised by NM, 18-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } → 𝐴 ∈ V )
3		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
4	3	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] 𝜑 )
5		sbcel12	⊢ ( [ 𝐴 / 𝑥 ] 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } )
6		csbvarg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝑥 = 𝐴 )
7	6	eleq1d	⊢ ( 𝐴 ∈ V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑥 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } ) )
8	5 7	bitrid	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } ) )
9	4 8	bitr3id	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } ) )
10	1 2 9	pm5.21nii	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } )