Theorem dfsbcq2 3740

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2711  [wsbc 3737

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738

This theorem is referenced by:  sbsbc  3741  sbc8g  3745  sbc2or  3746  sbceq1a  3748  sbc5ALT  3766  sbcng  3785  sbcimg  3786  sbcan  3787  sbcor  3788  sbcbig  3789  sbcim1  3791  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbctt  3807  sbcralt  3819  sbcreu  3823  rspsbc  3826  rspesbca  3828  sbcel12  4360  sbceqg  4361  csbif  4532  rexreusng  4631  sbcbr123  5147  opelopabsb  5473  csbopab  5498  csbopabgALT  5499  iota4  6467  csbiota  6479  csbriota  7324  onminex  7741  findes  7836  nn0ind-raph  12579  uzind4s  12808  nn0min  32808  sbcrexgOLD  42902