Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfsbcq2 | GIF version |
Description: This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb 1736 and substitution for class variables df-sbc 2910. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2911. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2202 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2126 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 2910 | . . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
4 | 3 | bicomi 131 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ [𝐴 / 𝑥]𝜑) |
5 | 1, 2, 4 | 3bitr3g 221 | 1 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1331 ∈ wcel 1480 [wsb 1735 {cab 2125 [wsbc 2909 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-clab 2126 df-cleq 2132 df-clel 2135 df-sbc 2910 |
This theorem is referenced by: sbsbc 2913 sbc8g 2916 sbceq1a 2918 sbc5 2932 sbcng 2949 sbcimg 2950 sbcan 2951 sbcang 2952 sbcor 2953 sbcorg 2954 sbcbig 2955 sbcal 2960 sbcalg 2961 sbcex2 2962 sbcexg 2963 sbcel1v 2971 sbctt 2975 sbcralt 2985 sbcrext 2986 sbcralg 2987 sbcreug 2989 rspsbc 2991 rspesbca 2993 sbcel12g 3017 sbceqg 3018 sbcbrg 3982 csbopabg 4006 opelopabsb 4182 findes 4517 iota4 5106 csbiotag 5116 csbriotag 5742 nn0ind-raph 9168 uzind4s 9385 bezoutlemmain 11686 bezoutlemex 11689 |
Copyright terms: Public domain | W3C validator |