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

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]˙ φ

Proof

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]˙ φ