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

Metamath Proof Explorer

Theorem csbopab

Description: Move substitution into a class abstraction. Version of csbopabgALT without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbopab ⊢ ⦋ A / x⦌ y z | φ = y z | [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ w = A → ⦋ w / x⦌ y z | φ = ⦋ A / x⦌ y z | φ
2 dfsbcq2 ⊢ w = A → w x φ ↔ [˙A / x]˙ φ
3 2 opabbidv ⊢ w = A → y z | w x φ = y z | [˙A / x]˙ φ
4 1 3 eqeq12d ⊢ w = A → ⦋ w / x⦌ y z | φ = y z | w x φ ↔ ⦋ A / x⦌ y z | φ = y z | [˙A / x]˙ φ
5 vex ⊢ w ∈ V
6 nfs1v ⊢ Ⅎ x w x φ
7 6 nfopab ⊢ Ⅎ _ x y z | w x φ
8 sbequ12 ⊢ x = w → φ ↔ w x φ
9 8 opabbidv ⊢ x = w → y z | φ = y z | w x φ
10 5 7 9 csbief ⊢ ⦋ w / x⦌ y z | φ = y z | w x φ
11 4 10 vtoclg ⊢ A ∈ V → ⦋ A / x⦌ y z | φ = y z | [˙A / x]˙ φ
12 csbprc ⊢ ¬ A ∈ V → ⦋ A / x⦌ y z | φ = ∅
13 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
14 13 con3i ⊢ ¬ A ∈ V → ¬ [˙A / x]˙ φ
15 14 nexdv ⊢ ¬ A ∈ V → ¬ ∃ z [˙A / x]˙ φ
16 15 nexdv ⊢ ¬ A ∈ V → ¬ ∃ y ∃ z [˙A / x]˙ φ
17 opabn0 ⊢ y z | [˙A / x]˙ φ ≠ ∅ ↔ ∃ y ∃ z [˙A / x]˙ φ
18 17 necon1bbii ⊢ ¬ ∃ y ∃ z [˙A / x]˙ φ ↔ y z | [˙A / x]˙ φ = ∅
19 16 18 sylib ⊢ ¬ A ∈ V → y z | [˙A / x]˙ φ = ∅
20 12 19 eqtr4d ⊢ ¬ A ∈ V → ⦋ A / x⦌ y z | φ = y z | [˙A / x]˙ φ
21 11 20 pm2.61i ⊢ ⦋ A / x⦌ y z | φ = y z | [˙A / x]˙ φ