Theorem dfsbcq2 3733

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  [wsb 2073   ∈ wcel 2119  {cab 2718  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731

This theorem is referenced by:  sbsbc  3734  sbc8g  3738  sbc2or  3739  sbceq1a  3741  sbc5ALT  3759  sbcng  3777  sbcimg  3778  sbcan  3779  sbcor  3780  sbcbig  3781  sbcim1  3783  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbctt  3799  sbcralt  3811  sbcreu  3815  rspsbc  3818  rspesbca  3820  sbcel12  4346  sbceqg  4347  csbif  4519  rexreusng  4618  sbcbr123  5133  opelopabsb  5479  csbopab  5504  csbopabgALT  5505  iota4  6473  csbiota  6485  csbriota  7335  onminex  7752  findes  7847  nn0ind-raph  12627  uzind4s  12856  nn0min  32920