Theorem dfsbcq2 3781

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2822	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2711	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3779	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 223	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 313	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  [wsb 2068   ∈ wcel 2107  {cab 2710  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  sbsbc  3782  sbc8g  3786  sbc2or  3787  sbceq1a  3789  sbc5ALT  3807  sbcng  3828  sbcimg  3829  sbcan  3830  sbcor  3831  sbcbig  3832  sbcim1  3834  sbcal  3842  sbcex2  3843  sbcel1v  3849  sbctt  3854  sbcralt  3867  sbcreu  3871  rspsbc  3874  rspesbca  3876  sbcel12  4409  sbceqg  4410  csbif  4586  rexreusng  4684  sbcbr123  5203  opelopabsb  5531  csbopab  5556  csbopabgALT  5557  iota4  6525  csbiota  6537  csbriota  7381  onminex  7790  findes  7893  nn0ind-raph  12662  uzind4s  12892  nn0min  32026  sbcrexgOLD  41523