Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version |
Description: Show that df-sb 1743 and df-sbc 2938 are equivalent when the class term 𝐴 in df-sbc 2938 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1743 for proofs involving df-sbc 2938. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2157 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 2940 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 [wsb 1742 [wsbc 2937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-clab 2144 df-cleq 2150 df-clel 2153 df-sbc 2938 |
This theorem is referenced by: spsbc 2948 sbcid 2952 sbcco 2958 sbcco2 2959 sbcie2g 2970 eqsbc3 2976 sbcralt 3013 sbcrext 3014 sbnfc2 3091 csbabg 3092 cbvralcsf 3093 cbvrexcsf 3094 cbvreucsf 3095 cbvrabcsf 3096 isarep1 5256 finexdc 6847 ssfirab 6878 zsupcllemstep 11832 bezoutlemmain 11882 bdsbc 13444 |
Copyright terms: Public domain | W3C validator |