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

Metamath Proof Explorer

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 ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑥 ∣ 𝜑 } )