![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbsbc | Structured version Visualization version Unicode version |
Description: Show that df-sb 1809 and df-sbc 3280 are equivalent when the class term ![]() |
Ref | Expression |
---|---|
sbsbc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2462 |
. 2
![]() ![]() ![]() ![]() | |
2 | dfsbcq2 3282 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1680 ax-4 1693 ax-5 1769 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-clab 2449 df-cleq 2455 df-clel 2458 df-sbc 3280 |
This theorem is referenced by: spsbc 3292 sbcid 3296 sbcco 3302 sbcco2 3303 sbcie2g 3313 eqsbc3 3319 sbcralt 3352 cbvralcsf 3407 cbvreucsf 3409 cbvrabcsf 3410 sbnfc2 3808 csbab 3809 wfis2fg 5436 isarep1 5684 tfindes 6716 tfinds2 6717 iuninc 28225 suppss2fOLD 28286 suppss2f 28287 fmptdF 28304 disjdsct 28332 esumpfinvalf 28946 measiuns 29088 bnj580 29773 bnj985 29813 setinds2f 30474 frins2fg 30534 bj-sbeq 31548 bj-sbel1 31552 bj-snsetex 31602 poimirlem25 32010 poimirlem26 32011 fdc1 32120 exlimddvfi 32407 frege52b 36530 frege58c 36562 pm13.194 36807 pm14.12 36816 sbiota1 36829 onfrALTlem1 36958 csbabgOLD 37251 onfrALTlem1VD 37327 disjinfi 37506 ellimcabssub0 37735 |
Copyright terms: Public domain | W3C validator |