![]() |
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 1868 and df-sbc 3403 are equivalent when the class term 𝐴 in df-sbc 3403 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1868 for proofs involving df-sbc 3403. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2610 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 3405 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 [wsb 1867 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: spsbc 3415 sbcid 3419 sbcco 3425 sbcco2 3426 sbcie2g 3436 eqsbc3 3442 sbcralt 3477 cbvralcsf 3531 cbvreucsf 3533 cbvrabcsf 3534 sbnfc2 3959 csbab 3960 wfis2fg 5634 isarep1 5891 tfindes 6954 tfinds2 6955 iuninc 28761 suppss2f 28819 fmptdF 28836 disjdsct 28863 esumpfinvalf 29465 measiuns 29607 bnj580 30237 bnj985 30277 setinds2f 30928 frins2fg 30988 bj-sbeq 32088 bj-sbel1 32092 bj-snsetex 32144 poimirlem25 32604 poimirlem26 32605 fdc1 32712 exlimddvfi 33097 frege52b 37203 frege58c 37235 pm13.194 37635 pm14.12 37644 sbiota1 37657 onfrALTlem1 37784 csbabgOLD 38072 onfrALTlem1VD 38148 disjinfi 38375 ellimcabssub0 38684 |
Copyright terms: Public domain | W3C validator |