![]() |
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 1643 and substitution for class variables df-sbc 2759. Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq 2760. (Contributed by NM, 31-Dec-2016.) |
Ref | Expression |
---|---|
dfsbcq2 | ⊢ (y = A → ([y / x]φ ↔ [A / x]φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2097 | . 2 ⊢ (y = A → (y ∈ {x ∣ φ} ↔ A ∈ {x ∣ φ})) | |
2 | df-clab 2024 | . 2 ⊢ (y ∈ {x ∣ φ} ↔ [y / x]φ) | |
3 | df-sbc 2759 | . . 3 ⊢ ([A / x]φ ↔ A ∈ {x ∣ φ}) | |
4 | 3 | bicomi 123 | . 2 ⊢ (A ∈ {x ∣ φ} ↔ [A / x]φ) |
5 | 1, 2, 4 | 3bitr3g 211 | 1 ⊢ (y = A → ([y / x]φ ↔ [A / x]φ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 = wceq 1242 ∈ wcel 1390 [wsb 1642 {cab 2023 [wsbc 2758 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-clab 2024 df-cleq 2030 df-clel 2033 df-sbc 2759 |
This theorem is referenced by: sbsbc 2762 sbc8g 2765 sbceq1a 2767 sbc5 2781 sbcng 2797 sbcimg 2798 sbcan 2799 sbcang 2800 sbcor 2801 sbcorg 2802 sbcbig 2803 sbcal 2804 sbcalg 2805 sbcex2 2806 sbcexg 2807 sbc3ang 2814 sbcel1gv 2815 sbctt 2818 sbcralt 2828 sbcrext 2829 sbcralg 2830 sbcrexg 2831 sbcreug 2832 rspsbc 2834 rspesbca 2836 sbcel12g 2859 sbceqg 2860 sbcbrg 3804 csbopabg 3826 opelopabsb 3988 findes 4269 iota4 4828 csbiotag 4838 csbriotag 5423 nn0ind-raph 8131 uzind4s 8309 |
Copyright terms: Public domain | W3C validator |