![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfsbcq2 | Structured version Visualization version 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 1806 and substitution for class variables df-sbc 3256. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 3257. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2537 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-clab 2458 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-sbc 3256 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bicomi 207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | 3bitr3g 295 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 df-clab 2458 df-cleq 2464 df-clel 2467 df-sbc 3256 |
This theorem is referenced by: sbsbc 3259 sbc8g 3263 sbc2or 3264 sbceq1a 3266 sbc5 3280 sbcng 3296 sbcimg 3297 sbcan 3298 sbcor 3299 sbcbig 3300 sbcal 3305 sbcex2 3306 sbcel1v 3314 sbctt 3318 sbcralt 3328 sbcreu 3332 rspsbc 3334 rspesbca 3336 sbcel12 3776 sbceqg 3777 csbif 3922 sbcbr123 4447 opelopabsb 4711 csbopab 4733 csbopabgALT 4734 iota4 5571 csbiota 5582 csbriota 6282 onminex 6653 findes 6742 nn0ind-raph 11058 uzind4s 11242 nn0min 28459 sbcrexgOLD 35699 sbcangOLD 36960 sbcorgOLD 36961 sbcalgOLD 36973 sbcexgOLD 36974 sbcel12gOLD 36975 sbcel1gvOLD 37318 |
Copyright terms: Public domain | W3C validator |