Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbceqbid | Structured version Visualization version Unicode version |
Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
Ref | Expression |
---|---|
sbceqbid.1 | |
sbceqbid.2 |
Ref | Expression |
---|---|
sbceqbid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceqbid.1 | . . 3 | |
2 | sbceqbid.2 | . . . 4 | |
3 | 2 | abbidv 2741 | . . 3 |
4 | 1, 3 | eleq12d 2695 | . 2 |
5 | df-sbc 3436 | . 2 | |
6 | df-sbc 3436 | . 2 | |
7 | 4, 5, 6 | 3bitr4g 303 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 cab 2608 wsbc 3435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-sbc 3436 |
This theorem is referenced by: fpwwe2cbv 9452 fpwwe2lem2 9454 fpwwe2lem3 9455 fi1uzind 13279 fi1uzindOLD 13285 isprs 16930 isdrs 16934 istos 17035 isdlat 17193 issrg 18507 islmod 18867 fdc 33541 hdmap1ffval 37085 hdmap1fval 37086 hdmapffval 37118 hdmapfval 37119 hgmapffval 37177 hgmapfval 37178 sbccomieg 37357 rexrabdioph 37358 |
Copyright terms: Public domain | W3C validator |