Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version |
Description: Show that df-sb 1756 and df-sbc 2956 are equivalent when the class term 𝐴 in df-sbc 2956 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1756 for proofs involving df-sbc 2956. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2170 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 2958 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 [wsb 1755 [wsbc 2955 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-clab 2157 df-cleq 2163 df-clel 2166 df-sbc 2956 |
This theorem is referenced by: spsbc 2966 sbcid 2970 sbcco 2976 sbcco2 2977 sbcie2g 2988 eqsbc1 2994 sbcralt 3031 sbcrext 3032 sbnfc2 3109 csbabg 3110 cbvralcsf 3111 cbvrexcsf 3112 cbvreucsf 3113 cbvrabcsf 3114 isarep1 5284 finexdc 6880 ssfirab 6911 zsupcllemstep 11900 bezoutlemmain 11953 bdsbc 13893 |
Copyright terms: Public domain | W3C validator |