Theorem dfsbcq2 3330

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

Assertion

Ref	Expression
dfsbcq2

Proof of Theorem dfsbcq2

Step	Hyp	Ref	Expression
1		eleq1 2529	. 2
2		df-clab 2443	. 2
3		df-sbc 3328	. . 3
4	3	bicomi 202	. 2
5	1, 2, 4	3bitr3g 287	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  [wsb 1739  e.wcel 1818  {cab 2442  [.wsbc 3327

This theorem is referenced by:  sbsbc  3331  sbc8g  3335  sbc2or  3336  sbceq1a  3338  sbc5  3352  sbcng  3368  sbcimg  3369  sbcan  3370  sbcangOLD  3371  sbcor  3372  sbcorgOLD  3373  sbcbig  3374  sbcal  3379  sbcalgOLD  3380  sbcex2  3381  sbcexgOLD  3382  sbc3angOLD  3391  sbcel1v  3392  sbcel1gvOLD  3393  sbctt  3398  sbcralt  3408  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  rspsbc  3417  rspesbca  3419  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbif  3991  csbifgOLD  3992  sbcbr123  4503  sbcbrgOLD  4504  opelopabsb  4762  csbopab  4784  csbopabgALT  4785  iota4  5574  csbiota  5585  csbiotagOLD  5586  csbriota  6269  onminex  6642  findes  6730  nn0ind-raph  10989  uzind4s  11170  nn0min  27611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328