Theorem dfsbcq2 3777

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2902	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2802	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3775	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 226	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 315	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  [wsb 2069   ∈ wcel 2114  {cab 2801  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775

This theorem is referenced by:  sbsbc  3778  sbc8g  3782  sbc2or  3783  sbceq1a  3785  sbc5  3802  sbcng  3821  sbcimg  3822  sbcan  3823  sbcor  3824  sbcbig  3825  sbcal  3835  sbcex2  3836  sbcel1v  3841  sbcel1vOLD  3842  sbctt  3846  sbcralt  3857  sbcreu  3861  rspsbc  3864  rspesbca  3866  sbcel12  4362  sbceqg  4363  csbif  4524  rexreusng  4619  sbcbr123  5122  opelopabsb  5419  csbopab  5444  csbopabgALT  5445  iota4  6338  csbiota  6350  csbriota  7131  onminex  7524  findes  7614  nn0ind-raph  12085  uzind4s  12311  nn0min  30538  sbcrexgOLD  39389