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

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
2 elex ⊢ A ∈ ⦋ A / x⦌ x | φ → A ∈ V
3 abid ⊢ x ∈ x | φ ↔ φ
4 3 sbcbii ⊢ [˙A / x]˙ x ∈ x | φ ↔ [˙A / x]˙ φ
5 sbcel12 ⊢ [˙A / x]˙ x ∈ x | φ ↔ ⦋ A / x⦌ x ∈ ⦋ A / x⦌ x | φ
6 csbvarg ⊢ A ∈ V → ⦋ A / x⦌ x = A
7 6 eleq1d ⊢ A ∈ V → ⦋ A / x⦌ x ∈ ⦋ A / x⦌ x | φ ↔ A ∈ ⦋ A / x⦌ x | φ
8 5 7 bitrid ⊢ A ∈ V → [˙A / x]˙ x ∈ x | φ ↔ A ∈ ⦋ A / x⦌ x | φ
9 4 8 bitr3id ⊢ A ∈ V → [˙A / x]˙ φ ↔ A ∈ ⦋ A / x⦌ x | φ
10 1 2 9 pm5.21nii ⊢ [˙A / x]˙ φ ↔ A ∈ ⦋ A / x⦌ x | φ