Theorem dfsbcq2 3742

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

Assertion

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

Proof of Theorem dfsbcq2

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2739  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740

This theorem is used by:  sbsbc  3743  sbc8g  3747  sbc2or  3748  sbceq1a  3750  sbc5ALT  3768  sbcng  3786  sbcimg  3787  sbcan  3788  sbcor  3789  sbcbig  3790  sbcim1  3792  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbctt  3808  sbcralt  3819  sbcreu  3823  rspsbc  3826  rspesbca  3828  sbcel12  4369  sbceqg  4370  csbif  4540  rexreusng  4640  sbcbr123  5159  opelopabsb  5504  csbopab  5530  csbopabw  5531  iota4  6512  csbiota  6524  csbriota  7384  onminex  7805  findes  7901  nn0ind-raph  12780  uzind4s  13016  nn0min  33394