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 ⊢ [˙A / x]˙ φ ↔ y ∈ ⦋ A / x⦌ y | φ

Proof

Step Hyp Ref Expression
1 abid ⊢ y ∈ y | φ ↔ φ
2 1 sbcbii ⊢ [˙A / x]˙ y ∈ y | φ ↔ [˙A / x]˙ φ
3 sbcel2 ⊢ [˙A / x]˙ y ∈ y | φ ↔ y ∈ ⦋ A / x⦌ y | φ
4 2 3 bitr3i ⊢ [˙A / x]˙ φ ↔ y ∈ ⦋ A / x⦌ y | φ