![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > dfsbcq2 | Unicode version |
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.) |
Ref | Expression |
---|---|
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 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |