Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbsbc | GIF version |
Description: Show that df-sb 1646 and df-sbc 2765 are equivalent when the class term 𝐴 in df-sbc 2765 is a setvar variable. This theorem lets us reuse theorems based on df-sb 1646 for proofs involving df-sbc 2765. (Contributed by NM, 31-Dec-2016.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
sbsbc | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2040 | . 2 ⊢ 𝑦 = 𝑦 | |
2 | dfsbcq2 2767 | . 2 ⊢ (𝑦 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 [wsb 1645 [wsbc 2764 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-clab 2027 df-cleq 2033 df-clel 2036 df-sbc 2765 |
This theorem is referenced by: spsbc 2775 sbcid 2779 sbcco 2785 sbcco2 2786 sbcie2g 2796 eqsbc3 2802 sbcralt 2834 sbcrext 2835 sbnfc2 2906 csbabg 2907 cbvralcsf 2908 cbvrexcsf 2909 cbvreucsf 2910 cbvrabcsf 2911 isarep1 4985 bdsbc 9978 |
Copyright terms: Public domain | W3C validator |