Theorem dfsbcq2 3686

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

Assertion

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

Proof of Theorem dfsbcq2

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  [wsb 2072   ∈ wcel 2112  {cab 2714  [wsbc 3683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-clab 2715  df-cleq 2728  df-clel 2809  df-sbc 3684

This theorem is referenced by:  sbsbc  3687  sbc8g  3691  sbc2or  3692  sbceq1a  3694  sbc5ALT  3712  sbcng  3733  sbcimg  3734  sbcan  3735  sbcor  3736  sbcbig  3737  sbcal  3747  sbcex2  3748  sbcel1v  3753  sbctt  3758  sbcralt  3771  sbcreu  3775  rspsbc  3778  rspesbca  3780  sbcel12  4309  sbceqg  4310  csbif  4482  rexreusng  4581  sbcbr123  5093  opelopabsb  5396  csbopab  5421  csbopabgALT  5422  iota4  6339  csbiota  6351  csbriota  7164  onminex  7564  findes  7658  nn0ind-raph  12242  uzind4s  12469  nn0min  30808  sbcrexgOLD  40251