![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version |
Description: Show that df-sb 1773 and df-sbc 2975 are equivalent when the class term 𝐴 in df-sbc 2975 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1773 for proofs involving df-sbc 2975. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2187 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 2977 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 [wsb 1772 [wsbc 2974 |
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 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-4 1520 ax-17 1536 ax-ial 1544 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-clab 2174 df-cleq 2180 df-clel 2183 df-sbc 2975 |
This theorem is referenced by: spsbc 2986 sbcid 2990 sbcco 2996 sbcco2 2997 sbcie2g 3008 eqsbc1 3014 sbcralt 3051 sbcrext 3052 sbnfc2 3129 csbabg 3130 cbvralcsf 3131 cbvrexcsf 3132 cbvreucsf 3133 cbvrabcsf 3134 isarep1 5314 finexdc 6915 ssfirab 6946 zsupcllemstep 11959 bezoutlemmain 12012 bdsbc 14881 |
Copyright terms: Public domain | W3C validator |