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 2905. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2906. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2200 | . 2 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-clab 2124 | . 2 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) | |
3 | df-sbc 2905 | . . 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 2123 [wsbc 2904 |
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 2119 |
This theorem depends on definitions: df-bi 116 df-clab 2124 df-cleq 2130 df-clel 2133 df-sbc 2905 |
This theorem is referenced by: sbsbc 2908 sbc8g 2911 sbceq1a 2913 sbc5 2927 sbcng 2944 sbcimg 2945 sbcan 2946 sbcang 2947 sbcor 2948 sbcorg 2949 sbcbig 2950 sbcal 2955 sbcalg 2956 sbcex2 2957 sbcexg 2958 sbcel1v 2966 sbctt 2970 sbcralt 2980 sbcrext 2981 sbcralg 2982 sbcreug 2984 rspsbc 2986 rspesbca 2988 sbcel12g 3012 sbceqg 3013 sbcbrg 3977 csbopabg 4001 opelopabsb 4177 findes 4512 iota4 5101 csbiotag 5111 csbriotag 5735 nn0ind-raph 9161 uzind4s 9378 bezoutlemmain 11675 bezoutlemex 11678 |
Copyright terms: Public domain | W3C validator |