Metamath Proof Explorer

Theorem dfsbcq2

Description: This theorem, which is similar to Theorem 6.7 of Quine p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb and substitution for class variables df-sbc . Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq . (Contributed by NM, 31-Dec-2016)

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


Step Hyp Ref Expression
1 eleq1 y = A y x | φ A x | φ
2 df-clab y x | φ y x φ
3 df-sbc [˙A / x]˙ φ A x | φ
4 3 bicomi A x | φ [˙A / x]˙ φ
5 1 2 4 3bitr3g y = A y x φ [˙A / x]˙ φ