Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version |
Description: Show that df-sb 1721 and df-sbc 2883 are equivalent when the class term 𝐴 in df-sbc 2883 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1721 for proofs involving df-sbc 2883. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2117 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 2885 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 [wsb 1720 [wsbc 2882 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-clab 2104 df-cleq 2110 df-clel 2113 df-sbc 2883 |
This theorem is referenced by: spsbc 2893 sbcid 2897 sbcco 2903 sbcco2 2904 sbcie2g 2914 eqsbc3 2920 sbcralt 2957 sbcrext 2958 sbnfc2 3030 csbabg 3031 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 isarep1 5179 finexdc 6764 ssfirab 6790 zsupcllemstep 11565 bezoutlemmain 11613 bdsbc 12983 |
Copyright terms: Public domain | W3C validator |