Metamath Proof Explorer


Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

Ref Expression
Assertion csbab A / x y | φ = y | [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 df-clab z y | [˙A / x]˙ φ z y [˙A / x]˙ φ
2 sbsbc z y [˙A / x]˙ φ [˙z / y]˙ [˙A / x]˙ φ
3 1 2 bitri z y | [˙A / x]˙ φ [˙z / y]˙ [˙A / x]˙ φ
4 sbccom [˙z / y]˙ [˙A / x]˙ φ [˙A / x]˙ [˙z / y]˙ φ
5 df-clab z y | φ z y φ
6 sbsbc z y φ [˙z / y]˙ φ
7 5 6 bitri z y | φ [˙z / y]˙ φ
8 7 sbcbii [˙A / x]˙ z y | φ [˙A / x]˙ [˙z / y]˙ φ
9 4 8 bitr4i [˙z / y]˙ [˙A / x]˙ φ [˙A / x]˙ z y | φ
10 sbcel2 [˙A / x]˙ z y | φ z A / x y | φ
11 3 9 10 3bitrri z A / x y | φ z y | [˙A / x]˙ φ
12 11 eqriv A / x y | φ = y | [˙A / x]˙ φ