Theorem dfsbcq2 3714

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2872	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2778	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3712	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 225	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 314	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1525  [wsb 2044   ∈ wcel 2083  {cab 2777  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-clab 2778  df-cleq 2790  df-clel 2865  df-sbc 3712

This theorem is referenced by:  sbsbc  3715  sbc8g  3719  sbc2or  3720  sbceq1a  3722  sbc5  3736  sbcng  3753  sbcimg  3754  sbcan  3755  sbcor  3756  sbcbig  3757  sbcal  3767  sbcex2  3768  sbcel1v  3773  sbcel1vOLD  3774  sbctt  3778  sbcralt  3789  sbcreu  3793  rspsbc  3796  rspesbca  3798  sbcel12  4286  sbceqg  4287  csbif  4442  rexreusng  4530  sbcbr123  5022  opelopabsb  5314  csbopab  5337  csbopabgALT  5338  iota4  6214  csbiota  6225  csbriota  6996  onminex  7385  findes  7475  nn0ind-raph  11936  uzind4s  12161  nn0min  30217  sbcrexgOLD  38888