Theorem dfsbcq2 3756

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

Assertion

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

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2857	. 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
2		df-clab 2748	. 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-sbc 3754	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
4	3	bicomi 227	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑)
5	1, 2, 4	3bitr3g 316	1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  [wsb 2097   ∈ wcel 2149  {cab 2747  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754

This theorem is referenced by:  sbsbc  3757  sbc8g  3761  sbc2or  3762  sbceq1a  3764  sbc5ALT  3782  sbcng  3800  sbcimg  3801  sbcan  3802  sbcor  3803  sbcbig  3804  sbcim1  3806  sbcal  3812  sbcex2  3813  sbcel1v  3818  sbctt  3822  sbcralt  3834  sbcreu  3838  rspsbc  3841  rspesbca  3843  sbcel12  4382  sbceqg  4383  csbif  4550  rexreusng  4650  sbcbr123  5169  opelopabsb  5517  csbopab  5543  csbopabw  5544  iota4  6520  csbiota  6532  csbriota  7385  onminex  7803  findes  7899  nn0ind-raph  12698  uzind4s  12934  nn0min  33108