Theorem dfsbcq2 3011

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 1789 and substitution for class variables df-sbc 3009. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3010. (Contributed by NM, 31-Dec-2016.)

Assertion

Ref	Expression
dfsbcq2	⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2272	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2196	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3009	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 132	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 222	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375  [wsb 1788   ∈ wcel 2180  {cab 2195  [wsbc 3008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-clab 2196  df-cleq 2202  df-clel 2205  df-sbc 3009

This theorem is referenced by:  sbsbc  3012  sbc8g  3016  sbceq1a  3018  sbc5  3032  sbcng  3049  sbcimg  3050  sbcan  3051  sbcang  3052  sbcor  3053  sbcorg  3054  sbcbig  3055  sbcal  3060  sbcalg  3061  sbcex2  3062  sbcexg  3063  sbcel1v  3071  sbctt  3075  sbcralt  3085  sbcrext  3086  sbcralg  3087  sbcreug  3089  rspsbc  3092  rspesbca  3094  sbcel12g  3119  sbceqg  3120  sbcbrg  4117  csbopabg  4141  opelopabsb  4327  findes  4672  iota4  5274  csbiotag  5287  csbriotag  5941  nn0ind-raph  9532  uzind4s  9753  bezoutlemmain  12485  bezoutlemex  12488