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 1881 and df-sbc 3436 are equivalent when the class term in df-sbc 3436 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1881 for proofs involving df-sbc 3436. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2622 | . 2 | |
2 | dfsbcq2 3438 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wsb 1880 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-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-clab 2609 df-cleq 2615 df-clel 2618 df-sbc 3436 |
This theorem is referenced by: spsbc 3448 sbcid 3452 sbcco 3458 sbcco2 3459 sbcie2g 3469 eqsbc3 3475 sbcralt 3510 cbvralcsf 3565 cbvreucsf 3567 cbvrabcsf 3568 sbnfc2 4007 csbab 4008 wfis2fg 5717 isarep1 5977 tfindes 7062 tfinds2 7063 iuninc 29379 suppss2f 29439 fmptdF 29456 disjdsct 29480 esumpfinvalf 30138 measiuns 30280 bnj580 30983 bnj985 31023 setinds2f 31684 frins2fg 31744 bj-sbeq 32896 bj-sbel1 32900 bj-snsetex 32951 poimirlem25 33434 poimirlem26 33435 fdc1 33542 exlimddvfi 33927 frege52b 38183 frege58c 38215 pm13.194 38613 pm14.12 38622 sbiota1 38635 onfrALTlem1 38763 csbabgOLD 39050 onfrALTlem1VD 39126 disjinfi 39380 ellimcabssub0 39849 |
Copyright terms: Public domain | W3C validator |