![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbsbc | Structured version Visualization version GIF version |
Description: Show that df-sb 2012 and df-sbc 3652 are equivalent when the class term 𝐴 in df-sbc 3652 is a setvar variable. This theorem lets us reuse theorems based on df-sb 2012 for proofs involving df-sbc 3652. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2777 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 3654 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 [wsb 2011 [wsbc 3651 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-clab 2763 df-cleq 2769 df-clel 2773 df-sbc 3652 |
This theorem is referenced by: spsbc 3664 sbcid 3668 sbcco 3674 sbcco2 3675 sbcie2g 3685 eqsbc3 3691 eqsbc3OLD 3692 sbcralt 3727 cbvralcsf 3782 cbvreucsf 3784 cbvrabcsf 3785 sbnfc2 4232 csbab 4233 wfis2fg 5970 isarep1 6222 tfindes 7340 tfinds2 7341 iuninc 29941 suppss2f 30004 fmptdF 30021 disjdsct 30046 esumpfinvalf 30736 measiuns 30878 bnj580 31582 bnj985 31622 setinds2f 32272 frins2fg 32336 bj-sbeq 33467 bj-sbel1 33471 bj-snsetex 33523 poimirlem25 34044 poimirlem26 34045 fdc1 34150 exlimddvfi 34533 frege52b 39121 frege58c 39153 pm13.194 39550 pm14.12 39559 sbiota1 39572 onfrALTlem1 39690 onfrALTlem1VD 40041 disjinfi 40285 ellimcabssub0 40739 2reu8i 42136 |
Copyright terms: Public domain | W3C validator |