| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version | ||
| Description: Show that df-sb 1785 and df-sbc 2998 are equivalent when the class term 𝐴 in df-sbc 2998 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1785 for proofs involving df-sbc 2998. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
| Ref | Expression |
|---|---|
| sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2204 | . 2 ⊢ 𝑦 = 𝑦 | |
| 2 | dfsbcq2 3000 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
| Colors of variables: wff set class |
| Syntax hints: ↔ wb 105 [wsb 1784 [wsbc 2997 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1469 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-4 1532 ax-17 1548 ax-ial 1556 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-clab 2191 df-cleq 2197 df-clel 2200 df-sbc 2998 |
| This theorem is referenced by: spsbc 3009 sbcid 3013 sbcco 3019 sbcco2 3020 sbcie2g 3031 eqsbc1 3037 sbcralt 3074 sbcrext 3075 sbnfc2 3153 csbabg 3154 cbvralcsf 3155 cbvrexcsf 3156 cbvreucsf 3157 cbvrabcsf 3158 isarep1 5359 finexdc 6998 ssfirab 7032 zsupcllemstep 10370 bezoutlemmain 12290 bdsbc 15756 |
| Copyright terms: Public domain | W3C validator |